--- a/CookBook/NamedThms.thy	Wed Oct 01 15:40:20 2008 -0400
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-
-theory NamedThms
-imports Main
-begin
-
-
-chapter {* Recipes *}
-
-text_raw {* 
-
-\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
-  
-
-
-