changeset 15 | 9da9ba2b095b |
parent 14 | 1c17e99f6f66 |
child 20 | 5ae6a1bb91c9 |
--- a/CookBook/Recipes/NamedThms.thy Wed Oct 01 20:42:55 2008 -0400 +++ b/CookBook/Recipes/NamedThms.thy Thu Oct 02 04:48:41 2008 -0400 @@ -1,9 +1,10 @@ theory NamedThms imports Main +uses "antiquote_setup.ML" + "antiquote_setup_plus.ML" begin - section {* Accumulate a List of Theorems under a Name *} @@ -53,6 +54,12 @@ \end{readmore} *} +text {* + (FIXME: maybe add a comment about the case when the theorems + to be added need to satisfy certain properties) + +*} + end