diff -r 28a49fe024c9 -r 304426a9aecf ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Nov 03 13:57:03 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Thu Nov 05 10:30:59 2009 +0100
@@ -89,7 +89,7 @@
   \end{quote}
 
   However, both commands will only play minor roles in this tutorial (we will
-  always arrange that the ML-code is defined outside of proofs).
+  always arrange that the ML-code is defined outside proofs).
 
   Once a portion of code is relatively stable, you usually want to export it
   to a separate ML-file. Such files can then be included somewhere inside a 
@@ -130,7 +130,7 @@
 section {* Printing and Debugging\label{sec:printing} *}
 
 text {*
-  During development you might find it necessary to inspect some data in your
+  During development you might find it necessary to inspect data in your
   code. This can be done in a ``quick-and-dirty'' fashion using the function
   @{ML_ind writeln in Output}. For example
 
@@ -156,7 +156,7 @@
   @{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}
 
   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
+  "foo"} is printed to a separate file, e.g., in order to prevent ProofGeneral from
   choking on massive amounts of trace output. This redirection can be achieved
   with the code:
 *}
@@ -219,7 +219,7 @@
   thm}. Isabelle contains elaborate pretty-printing functions for printing
   them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
   are a bit unwieldy. One way to transform a term into a string is to use the
-  function @{ML_ind  string_of_term in Syntax} in the structure @{ML_struct
+  function @{ML_ind  string_of_term in Syntax} from the structure @{ML_struct
   Syntax}. For more convenience, we bind this function to the toplevel.
 *}
 
@@ -254,8 +254,8 @@
   commas (map (string_of_term ctxt) ts)*}
 
 text {*
-  You can also print out term together with type information.
-  This can be achieved by setting the reference @{ML_ind show_types in Syntax} 
+  You can also print out terms together with typing information.
+  For this you need to set the reference @{ML_ind show_types in Syntax} 
   to @{ML true}.
 *}
 
@@ -270,7 +270,8 @@
 
   where @{text 1} and @{text x} are displayed with their inferred type.
   Even more type information can be printed by setting 
-  @{ML_ind show_all_types in Syntax} to @{ML true}. We obtain then
+  the reference @{ML_ind show_all_types in Syntax} to @{ML true}. 
+  We obtain then
 *}
 (*<*)ML %linenos {*show_all_types := true*}
 (*>*)
@@ -279,6 +280,7 @@
   "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
   "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
 
+  where @{term Pair} is the term-constructor for products. 
   Other references that influence printing are @{ML_ind show_brackets in Syntax} 
   and @{ML_ind show_sorts in Syntax}. 
 *}
@@ -336,7 +338,7 @@
   string_of_term ctxt (prop_of (no_vars ctxt thm))*}
 
 text {* 
-  Theorem @{thm [source] conjI} is now printed as follows:
+  With this function, theorem @{thm [source] conjI} is now printed as follows:
 
   @{ML_response_fake [display, gray]
   "tracing (string_of_thm_no_vars @{context} @{thm conjI})"
@@ -359,7 +361,7 @@
   @{ML_file "Pure/Syntax/printer.ML"}.
   \end{readmore}
 
-  Note that when printing out several ``parcels'' of information that
+  Note that for printing out several ``parcels'' of information that
   semantically belong together, like a warning message consisting of 
   a term and its type, you should try to keep this information together in a
   single string. Therefore do \emph{not} print out information as
@@ -378,15 +380,16 @@
 and second half."}
   
   To ease this kind of string manipulations, there are a number
-  of library functions. For example,  the function @{ML_ind cat_lines in Library}
-  concatenates a list of strings and inserts newlines. 
+  of library functions in Isabelle. For example,  the function 
+  @{ML_ind cat_lines in Library} concatenates a list of strings 
+  and inserts newlines in between each element. 
 
   @{ML_response [display, gray]
   "cat_lines [\"foo\", \"bar\"]"
   "\"foo\\nbar\""}
 
-  Section \ref{sec:pretty} will also explain the infrastructure of Isabelle 
-  that helps with more elaborate pretty printing. 
+  Section \ref{sec:pretty} will also explain the infrastructure that Isabelle 
+  provides for more elaborate pretty printing. 
 
   \begin{readmore}
   Most of the basic string functions of Isabelle are defined in 
@@ -508,6 +511,7 @@
   function @{ML_ind list_comb in Term} to the term. In this last step we have
   to use the function @{ML_ind curry in Library}, because @{ML list_comb}
   expects the function and the variables list as a pair. 
+  
   Functions like @{ML apply_fresh_args} are often needed when constructing 
   terms with fresh variables. The
   infrastructure helps tremendously to avoid any name clashes. Consider for
@@ -531,9 +535,9 @@
 *}
 
 ML{*val inc_by_six = 
-      (fn x => x + 1)
-   #> (fn x => x + 2)
-   #> (fn x => x + 3)*}
+  (fn x => x + 1) #> 
+  (fn x => x + 2) #> 
+  (fn x => x + 3)*}
 
 text {* 
   which is the function composed of first the increment-by-one function and then