--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Wed Oct 01 20:09:45 2008 -0400
@@ -0,0 +1,61 @@
+
+theory NamedThms
+imports Main
+begin
+
+
+section {* Accumulate a List of Theorems under a Name *} 
+
+
+text {*
+  \paragraph{Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules.
+
+  Users should be able to declare @{text foo}-rules in the theory,
+  which are then used by some method.
+
+  \paragraph{Solution:}
+
+  *}
+ML {*
+  structure FooRules = NamedThmsFun(
+    val name = "foo" 
+    val description = "Rules for foo"
+  );
+*}
+
+setup FooRules.setup
+
+text {*
+  This declares a context data slot where the theorems are stored,
+  an attribute @{attribute foo} (with the usual @{text add} and @{text del} options
+  to declare new rules, and the internal ML interface to retrieve and 
+  modify the facts.
+
+  Furthermore, the facts are made available under the dynamic fact name
+  @{text foo}:
+*}
+
+lemma rule1[foo]: "A" sorry
+lemma rule2[foo]: "B" sorry
+
+declare rule1[foo del]
+
+thm foo
+
+ML {* 
+  FooRules.get @{context};
+*}
+
+
+text {* 
+  \begin{readmore}
+  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+  \end{readmore}
+ *}
+
+
+end
+  
+
+
+