CookBook/Recipes/Antiquotes.thy
changeset 154 e81ebb37aa83
parent 153 c22b507e1407
child 165 890fbfef6d6b
equal deleted inserted replaced
153:c22b507e1407 154:e81ebb37aa83
   164   of this antiquotation, however, is that the hints can only be given in case
   164   of this antiquotation, however, is that the hints can only be given in case
   165   they can be constructed as a pattern. This excludes values that are abstract datatypes, like 
   165   they can be constructed as a pattern. This excludes values that are abstract datatypes, like 
   166   theorems or cterms.
   166   theorems or cterms.
   167 
   167 
   168 *}
   168 *}
   169 
       
   170 
       
   171 end
   169 end
   172   
   170   
   173 
   171 
   174 
   172 
   175 
   173