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 |