CookBook/Recipes/NamedThms.thy
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