--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/NamedThms.thy	Wed Sep 03 18:12:36 2008 +0200
@@ -0,0 +1,64 @@
+
+theory NamedThms
+imports Main
+begin
+
+text_raw {* 
+\newpage
+
+\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}
+  XXX
+
+  \end{readmore}
+ *}
+
+
+end
+  
+
+
+