--- a/CookBook/FirstSteps.thy	Mon Feb 09 01:23:35 2009 +0000
+++ b/CookBook/FirstSteps.thy	Mon Feb 09 04:18:14 2009 +0000
@@ -43,7 +43,7 @@
   value and function bindings, and even those can be undone when the proof
   script is retracted. As mentioned earlier, we will drop the
   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
-  show code. The lines prefixed with @{text ">"} are not part of the
+  show code. The lines prefixed with @{text [quotes] ">"} are not part of the
   code, rather they indicate what the response is when the code is evaluated.
 
   Once a portion of code is relatively stable, you usually want to export it
@@ -75,7 +75,7 @@
   will print out @{text [quotes] "any string"} inside the response buffer
   of Isabelle.  This function expects a string as argument. If you develop under PolyML,
   then there is a convenient, though again ``quick-and-dirty'', method for
-  converting values into strings, namely using the function @{ML makestring}:
+  converting values into strings, namely the function @{ML makestring}:
 
   @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 
 
@@ -92,7 +92,7 @@
 
   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 
   printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive 
-  amounts of trace output. This redirection can be achieved using the code
+  amounts of trace output. This redirection can be achieved with the code:
 *}
 
 ML{*val strip_specials =
@@ -112,12 +112,12 @@
   Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
   will cause that all tracing information is printed into the file @{text "foo.bar"}.
 
-  You can print out error messages with the function @{ML error}, as in:
+  You can print out error messages with the function @{ML error}; for example:
 
   @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
 
   Section~\ref{sec:printing} will give more information about printing 
-  the main datas tructures of Isabelle, namely @{ML_type term}, @{ML_type cterm} 
+  the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} 
   and @{ML_type thm}.
 *}
 
@@ -161,7 +161,7 @@
 
   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
 
-  or simpsets:
+  and simpsets:
 
   @{ML_response_fake [display,gray] 
 "let
@@ -385,8 +385,9 @@
   number representing their sum.
   \end{exercise}
 
-  (FIXME: maybe should go)
-
+  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} into an @{typ int} using the function
 *}
 
 ML{*fun nat_to_int t =
@@ -396,6 +397,8 @@
    | _ => t)*}
 
 text {*
+  an then apply it as follows:
+
 
 @{ML_response_fake [display,gray] 
 "map_types nat_to_int @{term \"a = (1::nat)\"}" 
@@ -424,7 +427,7 @@
 
   @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
 
-  This can also be wirtten with an antiquotation:
+  This can also be written with an antiquotation:
 
   @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
 
@@ -458,7 +461,9 @@
 text {*
   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
   that can only be built by going through interfaces. As a consequence, every proof 
-  in Isabelle is correct by construction (FIXME reference LCF-philosophy)
+  in Isabelle is correct by construction. 
+
+  (FIXME reference LCF-philosophy)
 
   To see theorems in ``action'', let us give a proof on the ML-level for the following 
   statement:
@@ -525,8 +530,8 @@
 section {* Printing Terms and Theorems\label{sec:printing} *}
 
 text {* 
-  During development, you often want to inspect terms, cterms 
-  or theorems. Isabelle contains elaborate pretty-printing functions for printing them, 
+  During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm} 
+  or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 
   but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 
   a term into a string is to use the function @{ML Syntax.string_of_term}.
 
@@ -535,7 +540,7 @@
   "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 
   This produces a string with some printing directions encoded in it. The string
-  can be properly printed by using @{ML warning} foe example.
+  can be properly printed by using the function @{ML warning}.
 
   @{ML_response_fake [display,gray]
   "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
@@ -746,7 +751,9 @@
 
 ML{*fun (x, y) |-> f = f x y*}
 
-text {* and can be used to write the following version of the @{text double} function *}
+text {* and can be used to write the following roundabout version 
+  of the @{text double} function 
+*}
 
 ML{*fun double x =
       x |>  (fn x => (x, x))