--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 09:18:46 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 12:13:21 2009 +0100
@@ -80,7 +80,7 @@
 
   @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 
 
-  However @{ML makestring} only works if the type of what is converted is monomorphic 
+  However, @{ML makestring} only works if the type of what is converted is monomorphic 
   and not a function.
 
   The function @{ML "warning"} should only be used for testing purposes, because any
@@ -92,7 +92,7 @@
   @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 
   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 
+  printed to a separate file, e.g., to prevent ProofGeneral from choking on massive 
   amounts of trace output. This redirection can be achieved with the code:
 *}
 
@@ -201,8 +201,8 @@
   Theorem @{thm [source] conjI} looks now as follows
 
   @{ML_response_fake [display, gray]
-  "warning (str_of_thm_raw @{context} @{thm conjI})"
-  "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+  "warning (str_of_thm @{context} @{thm conjI})"
+  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
   
   Again the function @{ML commas} helps with printing more than one theorem. 
 *}
@@ -251,7 +251,7 @@
     |> (fn x => x + 4)*}
 
 text {*
-  which increments its argument @{text x} by 5. It does this by first incrementing 
+  which increments its argument @{text x} by 5. It proceeds by first incrementing 
   the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 
   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
@@ -352,9 +352,9 @@
   cannot be merged back into the ``main waterfall''. To do this, you can use
   the next combinator.
 
-  The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
-  and returns the result together with the value (as a pair). For example
-  the function 
+  The combinator @{ML "`"} (a backtick) is similar to @{ML tap}, but applies a
+  function to the value and returns the result together with the value (as a
+  pair). For example the function 
 *}
 
 ML{*fun inc_as_pair x =
@@ -396,7 +396,8 @@
         |-> (fn x => fn y => x + y)*}
 
 text {*
-  Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 
+  Recall that @{ML "|>"} is the reverse function application. Recall also that
+  the related 
   reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
   composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 
@@ -412,7 +413,8 @@
   (FIXME: find a good exercise for combinators)
 
   \begin{readmore}
-  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+  The most frequently used combinators 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.
   \end{readmore}
@@ -486,20 +488,21 @@
   "get_thm_names_from_ss @{simpset}" 
   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
-  Again, this way or referencing simpsets makes you independent from additions
+  Again, this way of referencing simpsets makes you independent from additions
   of lemmas to the simpset by the user that potentially cause loops.
 
   On the ML-level of Isabelle, you often have to work with qualified names;
-  these are strings with some additional information, such positional information
+  these are strings with some additional information, such as positional information
   and qualifiers. Such bindings can be generated with the antiquotation 
-  @{text "@{bindin \<dots>}"}.
+  @{text "@{binding \<dots>}"}.
 
   @{ML_response [display,gray]
   "@{binding \"name\"}"
   "name"}
 
-  An example where a binding is needed is the function @{ML define in LocalTheory}.
-  Below this function defines the constant @{term "TrueConj"} as the conjunction
+  An example where a binding is needed is the function @{ML define in
+  LocalTheory}.  Below, this function is used to define the constant @{term
+  "TrueConj"} as the conjunction
   @{term "True \<and> True"}.
 *}
   
@@ -509,21 +512,21 @@
      (Attrib.empty_binding, @{term "True \<and> True"})) *}
 
 text {*
-  While antiquotations have many applications, they were originally introduced in order 
-  to avoid explicit bindings for theorems such as:
+  While antiquotations have many applications, they were originally introduced
+  in order to avoid explicit bindings of theorems such as:
 *}
 
 ML{*val allI = thm "allI" *}
 
 text {*
-  These bindings are difficult to maintain and also can be accidentally
-  overwritten by the user. This often broke Isabelle
+  Such bindings are difficult to maintain and can be overwritten by the
+  user accidentally. This often broke Isabelle
   packages. Antiquotations solve this problem, since they are ``linked''
   statically at compile-time.  However, this static linkage also limits their
   usefulness in cases where data needs to be build up dynamically. In the
-  course of this chapter you will learn more about these antiquotations:
+  course of this chapter you will learn more about antiquotations:
   they can simplify Isabelle programming since one can directly access all
-  kinds of logical elements from th ML-level.
+  kinds of logical elements from the ML-level.
 *}
 
 section {* Terms and Types *}
@@ -1360,4 +1363,4 @@
 
 ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
 
-end
\ No newline at end of file
+end