--- a/CookBook/FirstSteps.thy	Sun Oct 05 14:29:13 2008 -0400
+++ b/CookBook/FirstSteps.thy	Mon Oct 06 10:11:08 2008 -0400
@@ -24,7 +24,7 @@
   \end{center}
 *}
 
-section {* Inluding ML-Code *}
+section {* Including ML-Code *}
 
 text {*
   The easiest and quickest way to include code in a theory is
@@ -292,7 +292,7 @@
 text {*
 
   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 
-  @{term "tau"} into an antiquotation. For example this following does not work.
+  @{term "tau"} into an antiquotation. For example the following does not work.
 *}
 
 ML {*
@@ -323,6 +323,8 @@
 
   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 
+  (FIXME: how to construct types manually)
+
   \begin{readmore}
   There are many functions in @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
@@ -362,7 +364,7 @@
   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   Unlike @{ML_type term}s, which are just trees, @{ML_type
   "cterm"}s are abstract objects that are guaranteed to be
-  type-correct, and can only be constructed via the official
+  type-correct, and that can only be constructed via the official
   interfaces.
 
   Type checking is always relative to a theory context. For now we can use
@@ -372,6 +374,8 @@
 
 ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}
 
+text {* and *}
+
 ML {*
   let
     val natT = @{typ "nat"}
@@ -459,7 +463,6 @@
   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
 
   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals. 
-
   Since the goal @{term C} can potentially be an implication, there is a
   @{text "#"} wrapped around it, which prevents that premises are 
   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
@@ -540,6 +543,10 @@
 end
 *}
 
-section {* Storing and Changing Theorems and so on *}
+section {* Storing Theorems *}
+
+section {* Theorem Attributes *}
+
+text {* Was changing theorems. *}
 
 end
\ No newline at end of file

--- 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}

Binary file cookbook.pdf has changed