--- a/CookBook/Recipes/NamedThms.thy	Thu Feb 26 14:20:52 2009 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-theory NamedThms
-imports "../Base"
-begin
-
-section {* Accumulate a List of Theorems under a Name\label{rec:named} *} 
-
-
-text {*
-  {\bf 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 in a method.\smallskip
-
-  {\bf Solution:} This can be achieved using named theorem lists.\smallskip
-
-  Named theorem lists can be set up using the code
-
-  *}
-
-ML{*structure FooRules = NamedThmsFun (
-  val name = "foo" 
-  val description = "Rules for foo"); *}
-
-text {*
-  and the command
-*}
-
-setup {* FooRules.setup *}
-
-text {*
-  This code declares a context data slot where the theorems are stored,
-  an attribute @{text foo} (with the usual @{text add} and @{text del} options
-  for adding and deleting theorems) and an internal ML interface to retrieve and 
-  modify the theorems.
-
-  Furthermore, the facts are made available on the user level under the dynamic 
-  fact name @{text foo}. For example we can declare three lemmas to be of the kind
-  @{text foo} by:
-*}
-
-lemma rule1[foo]: "A" sorry
-lemma rule2[foo]: "B" sorry
-lemma rule3[foo]: "C" sorry
-
-text {* and undeclare the first one by: *}
-
-declare rule1[foo del]
-
-text {* and query the remaining ones with:
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "foo"}\\
-  @{text "> ?C"}\\
-  @{text "> ?B"}\\
-  \end{isabelle}
-
-  On the ML-level the rules marked with @{text "foo"} an be retrieved
-  using the function @{ML FooRules.get}:
-
-  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
-
-  \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
-  the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
-  data.
-  \end{readmore}
- *}
-
-text {*
-  (FIXME: maybe add a comment about the case when the theorems 
-  to be added need to satisfy certain properties)
-
-*}
-
-
-end
-  
-
-
-