--- a/CookBook/FirstSteps.thy	Thu Feb 05 22:44:11 2009 +0000
+++ b/CookBook/FirstSteps.thy	Fri Feb 06 06:19:52 2009 +0000
@@ -519,30 +519,30 @@
 section {* Printing Terms, CTerms and Theorems\label{sec:printing} *}
 
 text {* 
-  It will often be necesseary to inspect terms, cterms or theorems. Isabelle
-  contains elaborate pretty-printing functions for that, but for quick-and-dirty
-  solutions they are too unwieldy. A term can be transformed into a string using
-  the function @{ML Syntax.string_of_term}
+  You will occationally feel the need to inspect terms, cterms or theorems during
+  development. Isabelle contains elaborate pretty-printing functions for that, but 
+  for quick-and-dirty solutions they are way too unwieldy. A simple way to transform 
+  a term into a string is to use the function @{ML Syntax.string_of_term}.
 
   @{ML_response_fake [display,gray]
   "Syntax.string_of_term @{context} @{term \"1::nat\"}"
   "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 
-  This produces a string, though with printing directions encoded in it. This
-  can be properly printed, when enclosed in a @{ML warning}
+  This produces a string, though with printing directions encoded in it. The string
+  can be properly printed, when enclosed in a @{ML warning}.
 
   @{ML_response_fake [display,gray]
   "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
   "\"1\""}
 
-  A @{ML_type cterm} can be transformed into a string by the function:
+  A @{ML_type cterm} can be transformed into a string by the following function.
 *}
 
 ML{*fun str_of_cterm ctxt t =  
    Syntax.string_of_term ctxt (term_of t)*}
 
 text {*
-  If there are more than one @{ML_type cterm} to be printed, we can use the function
+  If there are more than one @{ML_type cterm} to be printed, you can use the function
   @{ML commas} to conveniently separate them.
 *} 
 
@@ -550,7 +550,7 @@
   commas (map (str_of_cterm ctxt) ts)*}
 
 text {*
-  The easiest way to get the string of a theorem, is to transform it
+  The easiest way to get the string of a theorem is to transform it
   into a @{ML_type cterm} using the function @{ML crep_thm}.
 *}
 
@@ -562,7 +562,7 @@
   end*}
 
 text {* 
-  For more than one theorem, the following function adds commas in between them. 
+  Again the function @{ML commas} helps with printing more than one theorem. 
 *}
 
 ML{*fun str_of_thms ctxt thms =  
@@ -604,7 +604,7 @@
   \begin{readmore}
   The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
   and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
-  contains further information about combinators.
+  contains further information about them.
   \end{readmore}
 
   The simplest combinator is @{ML I}, which is just the identity function.
@@ -618,10 +618,10 @@
 
 text {*
   @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 
-  function ignores its argument. As a result @{ML K} defines a constant function 
+  function ignores its argument. As a result, @{ML K} defines a constant function 
   returning @{text x}.
 
-  The next combinator is reverse application, @{ML "|>"}, defined as 
+  The next combinator is reverse application, @{ML "|>"}, defined as: 
 *}
 
 ML{*fun x |> f = f x*}
@@ -642,8 +642,8 @@
   the first component of the pair (Line 4) and finally incrementing the first 
   component by 4 (Line 5). This kind of cascading manipulations of values is quite
   common when dealing with theories (for example by adding a definition, followed by
-  lemmas and so on). The reverse application allows you to read what happens inside
-  the function in a top-down manner. This kind of codeing should also be familiar, 
+  lemmas and so on). The reverse application allows you to read what happens in 
+  a top-down manner. This kind of coding should also be familiar, 
   if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using 
   the reverse application is much clearer than writing
 *}