--- a/ProgTutorial/FirstSteps.thy	Wed Aug 05 16:00:01 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Thu Aug 13 21:32:10 2009 +0200
@@ -6,7 +6,7 @@
 
 text {*
   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
-  in Isabelle is part of a theory. If you want to follow the code given in
+  for Isabelle must be part of a theory. If you want to follow the code given in
   this chapter, we assume you are working inside the theory starting with
 
   \begin{quote}
@@ -158,16 +158,20 @@
      TextIO.flushOut stream)) *}
 
 text {*
-  Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
+  Calling now
+
+  @{ML [display,gray] "redirect_tracing (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 [index] error}; for example:
+  You can print out error messages with the function @{ML [index] error}; for 
+  example:\footnote{FIXME: unwanted pagebreak}
 
 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 
-  This function raises the exception @{text ERROR} which will then 
+  This function raises the exception @{text ERROR}, which will then 
   be displayed by the infrastructure.
 
 
@@ -193,7 +197,7 @@
   Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} 
   or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing 
   them (see Section \ref{sec:pretty}), 
-  but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 
+  but  for quick-and-dirty solutions they are far too unwieldy. One way to transform 
   a term into a string is to use the function @{ML [index] string_of_term in Syntax}.
 
   @{ML_response_fake [display,gray]
@@ -201,7 +205,8 @@
   "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 
   This produces a string with some additional information encoded in it. The string
-  can be properly printed by using the function @{ML [index] writeln}.
+  can be properly printed by using either the function @{ML [index] writeln} or 
+  @{ML [index] tracing}.
 
   @{ML_response_fake [display,gray]
   "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"
@@ -270,10 +275,10 @@
   commas (map (string_of_thm_no_vars ctxt) thms) *}
 
 text {*
-  When printing out several parcels of information that semantiaclly 
-  belong  together, like a warning message consisting of a term and
-  a type, you should try to keep this information together 
-  in a single string. So do not print out information as
+  When printing out several parcels of information that semantically 
+  belong  together, like a warning message consisting for example 
+  of a term and a type, you should try to keep this information 
+  together in a single string. So do not print out information as
 
 @{ML_response_fake [display,gray]
 "tracing \"First half,\";