--- a/ProgTutorial/FirstSteps.thy	Wed Aug 19 09:25:49 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Thu Aug 20 10:38:26 2009 +0200
@@ -239,13 +239,13 @@
   A @{ML_type cterm} can be transformed into a string by the following function.
 *}
 
-ML{*fun string_of_cterm ctxt t =  
-  string_of_term ctxt (term_of t)*}
+ML{*fun string_of_cterm ctxt ct =  
+  string_of_term ctxt (term_of ct)*}
 
 text {*
-  In this example the function @{ML [index] term_of} extracts the @{ML_type term} from
-  a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be printed
-  with @{ML [index] commas}.
+  In this example the function @{ML [index] term_of} extracts the @{ML_type
+  term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be
+  printed with @{ML [index] commas}.
 *} 
 
 ML{*fun string_of_cterms ctxt cts =  
@@ -261,16 +261,19 @@
 
 text {*
   Theorems also include schematic variables, such as @{text "?P"}, 
-  @{text "?Q"} and so on. 
+  @{text "?Q"} and so on. They are needed in order to able to
+  instantiate theorems when they are applied. For example the theorem 
+  @{thm [source] conjI} shown below can be used for any (typable) 
+  instantiation of @{text "?P"} and @{text "?Q"} 
 
   @{ML_response_fake [display, gray]
   "tracing (string_of_thm @{context} @{thm conjI})"
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
-  In order to improve the readability of theorems we convert these schematic
-  variables into free variables using the function @{ML [index] import in
-  Variable}. This is similar to statements like @{text "conjI[no_vars]"} 
-  from Isabelle's user-level.
+  However, in order to improve the readability when printing theorems, we
+  convert these schematic variables into free variables using the function
+  @{ML [index] import in Variable}. This is similar to statements like @{text
+  "conjI[no_vars]"} from Isabelle's user-level.
 *}
 
 ML{*fun no_vars ctxt thm =
@@ -300,10 +303,10 @@
   commas (map (string_of_thm_no_vars ctxt) thms) *}
 
 text {*
-  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
+  Note, that 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,\"; 
@@ -520,8 +523,8 @@
 ML{*fun (x, y) ||> f = (x, f y)*}
 
 text {*
-  These two functions can be used to avoid explicit @{text "lets"} for
-  intermediate values in functions that return pairs. Suppose for example you
+  These two functions can, for example, be used to avoid explicit @{text "lets"} for
+  intermediate values in functions that return pairs. As an example, suppose you
   want to separate a list of integers into two lists according to a
   treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
   should be separated to @{ML "([1,2,3,4], [6,5])"}.  This function can be
@@ -549,9 +552,9 @@
       else separate i xs |>> cons x*}
 
 text {*
-  avoiding the explicit @{text "let"}. While in this example the gain is only
-  small, in more complicated situations the benefit of avoiding @{text "lets"}
-  can be substantial.
+  avoiding the explicit @{text "let"}. While in this example the gain in
+  conciseness is only small, in more complicated situations the benefit of
+  avoiding @{text "lets"} can be substantial.
 
   With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair.
   This combinator is defined as
@@ -617,7 +620,7 @@
 
 
 text {* 
-  When using combinators for writing function in waterfall fashion, it is
+  When using combinators for writing functions in waterfall fashion, it is
   sometimes necessary to do some ``plumbing'' in order to fit functions
   together. We have already seen such plumbing in the function @{ML
   apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
@@ -643,9 +646,9 @@
   In this example we obtain two terms with appropriate typing. However, if you
   have only a single term, then @{ML check_terms in Syntax} needs to be
   adapted. This can be done with the ``plumbing'' function @{ML
-  singleton}.\footnote{There is in fact alread a function @{ML check_term in Syntax},
-  which however is defined in terms of @{ML singleton} and @{ML check_terms in
-  Syntax}.} For example
+  singleton}.\footnote{There is already a function @{ML check_term in Syntax}
+  in the Isabelle sources that is defined in terms of @{ML singleton} and @{ML
+  check_terms in Syntax}.} For example
 
   @{ML_response_fake [display, gray]
   "let