--- a/CookBook/FirstSteps.thy	Tue Feb 24 01:30:15 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Feb 24 11:15:41 2009 +0000
@@ -141,6 +141,7 @@
    Syntax.string_of_term ctxt (term_of t)*}
 
 text {*
+  The function @{ML term_of} extracts the @{ML_type term} from a @{ML_type cterm}.
   If there are more than one @{ML_type cterm}s to be printed, you can use the 
   function @{ML commas} to separate them.
 *} 
@@ -388,7 +389,7 @@
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  
 
-  You can also refer to the current simpsets. To illustrate this we use the
+  You can also refer to the current simpset. To illustrate this we use the
   function that extracts the theorem names stored in a simpset.
 *}
 
@@ -404,8 +405,9 @@
   information about the simpset. The rules of a simpset are stored in a
   \emph{discrimination net} (a data structure for fast indexing). From this
   net you can extract the entries using the function @{ML Net.entries}.
-  You can now use @{ML get_thm_names} to obtain all names of theorems of
-  the current simpset using the antiquotation @{text "@{simpset}"}.\footnote
+  You can now use @{ML get_thm_names} to obtain all names of theorems stored
+  in the current simpset---this simpset can be referred to using the antiquotation
+  @{text "@{simpset}"}.\footnote
   {FIXME: you cannot cleanly match against lists with ommited parts}
 
   @{ML_response_fake [display,gray] 
@@ -571,6 +573,25 @@
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
 text {*
+  A handy function for manipulating terms is @{ML map_types}: it takes a 
+  function and applies it to every type in the term. You can, for example,
+  change every @{typ nat} in a term into an @{typ int} using the function:
+*}
+
+ML{*fun nat_to_int t =
+  (case t of
+     @{typ nat} => @{typ int}
+   | Type (s, ts) => Type (s, map nat_to_int ts)
+   | _ => t)*}
+
+text {*
+  An example as follows:
+
+@{ML_response_fake [display,gray] 
+"map_types nat_to_int @{term \"a = (1::nat)\"}" 
+"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
+           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
+
   \begin{readmore}
   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
@@ -595,26 +616,6 @@
   number representing their sum.
   \end{exercise}
 
-  A handy function for manipulating terms is @{ML map_types}: it takes a 
-  function and applies it to every type in the term. You can, for example,
-  change every @{typ nat} in a term into an @{typ int} using the function:
-*}
-
-ML{*fun nat_to_int t =
-  (case t of
-     @{typ nat} => @{typ int}
-   | Type (s, ts) => Type (s, map nat_to_int ts)
-   | _ => t)*}
-
-text {*
-  An example as follows:
-
-@{ML_response_fake [display,gray] 
-"map_types nat_to_int @{term \"a = (1::nat)\"}" 
-"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
-           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
-
-
   There are a few subtle issues with constants. They usually crop up when
   pattern matching terms or types, or constructing them. While it is perfectly ok
   to write the function @{text is_true} as follows

--- a/CookBook/Tactical.thy	Tue Feb 24 01:30:15 2009 +0000
+++ b/CookBook/Tactical.thy	Tue Feb 24 11:15:41 2009 +0000
@@ -1025,7 +1025,7 @@
 text {*
   In Isabelle you can also implement custom simplification procedures, called
   \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and
-  rewrite a term according to theorem. They are useful in cases where
+  rewrite a term according to a theorem. They are useful in cases where
   a rewriting rule must be produced on ``demand'' or when rewriting by
   simplification is too unpredictable and potentially loops.
 
@@ -1232,7 +1232,7 @@
   @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 
   (Line 4), which it proves by the arithmetic tactic in Line 6. 
 
-  For our purpose at the moment, using in the code above @{ML arith_tac} is
+  For our purpose at the moment, proving the meta-equation using @{ML arith_tac} is
   fine, but there is also an alternative employing the simplifier with a very
   restricted simpset. For the kind of lemmas we want to prove, the simpset
   @{text "num_ss"} in the code will suffice.

Binary file cookbook.pdf has changed