--- a/CookBook/Recipes/NamedThms.thy	Sun Oct 05 14:29:13 2008 -0400
+++ b/CookBook/Recipes/NamedThms.thy	Mon Oct 06 10:11:08 2008 -0400
@@ -9,12 +9,12 @@
 
 
 text {*
-  \paragraph{Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules.
-
+  {\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 by some method.
+  which are then used by some method.\smallskip
 
-  \paragraph{Solution:}
+  {\bf Solution:} This can be achieved using 
 
   *}
 ML {*
@@ -27,13 +27,13 @@
 setup FooRules.setup
 
 text {*
-  This declares a context data slot where the theorems are stored,
+  This code 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.
+  to adding and deleting theorems) and an internal ML interface to retrieve and 
+  modify the theorems.
 
-  Furthermore, the facts are made available under the dynamic fact name
-  @{text foo}:
+  Furthermore, the facts are made available on the user level under the dynamic 
+  fact name @{text foo}. For example:
 *}
 
 lemma rule1[foo]: "A" sorry
@@ -43,10 +43,13 @@
 
 thm foo
 
-ML {* 
-  FooRules.get @{context};
+text {* 
+  In an ML-context the rules marked with @{text "foo"} an be retrieved
+  using
 *}
 
+ML {* FooRules.get @{context} *}
+
 
 text {* 
   \begin{readmore}