CookBook/FirstSteps.thy
changeset 132 2d9198bcb850
parent 131 8db9195bb3e9
child 133 3e94ccc0f31e
equal deleted inserted replaced
131:8db9195bb3e9 132:2d9198bcb850
   374   function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
   374   function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
   375   \emph{not} replaced with code that will look up the current theory in 
   375   \emph{not} replaced with code that will look up the current theory in 
   376   some data structure and return it. Instead, it is literally
   376   some data structure and return it. Instead, it is literally
   377   replaced with the value representing the theory name.
   377   replaced with the value representing the theory name.
   378 
   378 
   379   In a similar way you can use antiquotations to refer to proved theorems:
   379   In a similar way you can use antiquotations to refer to proved theorems: 
       
   380   for a single theorem
   380 
   381 
   381   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
   382   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
   382 
   383 
   383   and current simpsets. For this we use the function that extracts the 
   384   and for more than one
   384   theorem names stored in the simpset.
   385 
       
   386 @{ML_response_fake [display,gray] "@{thms conj_ac}" 
       
   387 "(?P \<and> ?Q) = (?Q \<and> ?P)
       
   388 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
       
   389 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  
       
   390 
       
   391   You can also refer to the current simpsets. To illustrate this we use the
       
   392   function that extracts the theorem names stored in a simpset.
   385 *}
   393 *}
   386 
   394 
   387 ML{*fun get_thm_names simpset =
   395 ML{*fun get_thm_names simpset =
   388 let
   396 let
   389   val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
   397   val ({rules,...}, _) = MetaSimplifier.rep_ss simpset