--- a/ProgTutorial/First_Steps.thy	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/First_Steps.thy	Wed Oct 15 23:12:54 2014 +0100
@@ -105,7 +105,7 @@
 
   @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 
 
-  However, @{text "@{makes_tring}"} only works if the type of what
+  However, @{text "@{make_string}"} only works if the type of what
   is converted is monomorphic and not a function. 
 
   You can print out error messages with the function @{ML_ind error in Library}; 
@@ -120,12 +120,12 @@
   be displayed by the infrastructure indicating that it is an error by
   painting the output red. Note that this exception is meant 
   for ``user-level'' error messages seen by the ``end-user''. 
-  For messages where you want to indicate a genuine program error, then
+  For messages where you want to indicate a genuine program error
   use the exception @{text Fail}. 
 
-  Most often you want to inspect data of Isabelle's basic data structures,
+  Most often you want to inspect contents of Isabelle's basic data structures,
   namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
-  and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
+  and @{ML_type thm}. Isabelle provides elaborate pretty-printing functions,
   which we will explain in more detail in Section \ref{sec:pretty}. For now
   we just use the functions @{ML_ind writeln in Pretty}  from the structure
   @{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure
@@ -136,7 +136,7 @@
 val pwriteln = Pretty.writeln*}
 
 text {*
-  They can now be used as follows
+  They can be used as follows
 
   @{ML_response_fake [display,gray]
   "pwriteln (pretty_term @{context} @{term \"1::nat\"})"
@@ -151,8 +151,8 @@
   Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
 
 text {*
-  You can also print out terms together with their typing information.
-  For this you need to set the configuration value  
+  To print out terms together with their typing information,
+  set the configuration value
   @{ML_ind show_types in Syntax} to @{ML true}.
 *}
 
@@ -165,7 +165,7 @@
   "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
   "(1::nat, x::'a)"}
 
-  where @{text 1} and @{text x} are displayed with their inferred type.
+  where @{text 1} and @{text x} are displayed with their inferred types.
   Other configuration values that influence
   printing of terms include 
 
@@ -200,8 +200,8 @@
 
 text {*
   Theorems include schematic variables, such as @{text "?P"}, 
-  @{text "?Q"} and so on. They are needed in Isabelle in order to able to
-  instantiate theorems when they are applied. For example the theorem 
+  @{text "?Q"} and so on. They are instantiated by Isabelle when a theorem is applied.
+  For example, the theorem 
   @{thm [source] conjI} shown below can be used for any (typable) 
   instantiation of @{text "?P"} and @{text "?Q"}. 
 
@@ -209,7 +209,7 @@
   "pwriteln (pretty_thm @{context} @{thm conjI})"
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
-  However, in order to improve the readability when printing theorems, we
+  However, to improve the readability when printing theorems, we
   can switch off the question marks as follows:
 *}
 
@@ -367,9 +367,9 @@
 in y4 end*}
 
 text {* 
-  Another reason why the let-bindings in the code above are better to be
-  avoided: it is more than easy to get the intermediate values wrong, not to 
-  mention the nightmares the maintenance of this code causes!
+  Another reasons to avoid the let-bindings in the code above:
+  it is easy to get the intermediate values wrong and
+  the resulting code is difficult to maintain.
 
   In Isabelle a ``real world'' example for a function written in 
   the waterfall fashion might be the following code:
@@ -384,9 +384,9 @@
       |> curry list_comb f *}
 
 text {*
-  This function takes a term and a context as argument. If the term is of function
+  This function takes a term and a context as arguments. If the term is of function
   type, then @{ML "apply_fresh_args"} returns the term with distinct variables 
-  applied to it. For example below three variables are applied to the term 
+  applied to it. For example, below three variables are applied to the term 
   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 
   @{ML_response_fake [display,gray]
@@ -463,7 +463,7 @@
 text {*
   The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 
   @{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory}; 
-  its purpose is to store a theorem under a name. 
+  it stores a theorem under a name. 
   In lines 5 to 6 we call this function to give alternative names for the three
   theorems. The point of @{ML "#>"} is that you can sequence such function calls. 
 
@@ -770,7 +770,7 @@
 
   Another important antiquotation is @{text "@{context}"}. (What the
   difference between a theory and a context is will be described in Chapter
-  \ref{chp:advanced}.) A context is for example needed in order to use the
+  \ref{chp:advanced}.) A context is for example needed to use the
   function @{ML print_abbrevs in Proof_Context} that list of all currently
   defined abbreviations. For example
 
@@ -853,8 +853,8 @@
 
   It is also possible to define your own antiquotations. But you should
   exercise care when introducing new ones, as they can also make your code
-  also difficult to read. In the next chapter we describe how to construct
-  terms with the (build in) antiquotation @{text "@{term \<dots>}"}.  A restriction
+  difficult to read. In the next chapter we describe how to construct
+  terms with the (built-in) antiquotation @{text "@{term \<dots>}"}.  A restriction
   of this antiquotation is that it does not allow you to use schematic
   variables in terms. If you want to have an antiquotation that does not have
   this restriction, you can implement your own using the function @{ML_ind
@@ -918,8 +918,8 @@
 setup %gray {* type_pat_setup *}
 
 text {* 
-However, a word of warning is in order: Introducing new antiquotations should be done only after
-careful deliberations. They can potentially make your code harder to read, than making it easier.
+However, a word of warning is in order: new antiquotations should be introduced only after
+careful deliberations. They can potentially make your code harder, rather than easier, to read.
 
   \begin{readmore}
   The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
@@ -1010,7 +1010,7 @@
   are only relevant to the proof at hand. Therefore such data needs to be 
   maintained inside a proof context, which represents ``local'' data.
   You can think of a theory as the ``longterm memory'' of Isabelle (nothing will
-  be deleted from it), and a proof-context as a ``shortterm memory'' (it dynamically
+  be deleted from it), and a proof-context as a ``shortterm memory'' (it
   changes according to what is needed at the time).
 
   For theories and proof contexts there are, respectively, the functors 
@@ -1042,7 +1042,7 @@
   defaults.\footnote{\bf FIXME: Say more about the
   assumptions of these operations.} The result structure @{ML_text Data}
   contains functions for accessing the table (@{ML Data.get}) and for updating
-  it (@{ML Data.map}). There is also the functions @{ML Data.put}, which however is 
+  it (@{ML Data.map}). There is also the function @{ML Data.put}, but it is 
   not relevant here. Below we define two
   auxiliary functions, which help us with accessing the table.
 *}
@@ -1064,7 +1064,7 @@
 text {*
   The use of the command \isacommand{setup} makes sure the table in the 
   \emph{current} theory is updated (this is explained further in 
-  section~\ref{sec:theories}). The lookup can now be performed as follows.
+  Section~\ref{sec:theories}). The lookup can now be performed as follows.
 
   @{ML_response_fake [display, gray]
 "lookup @{theory} \"conj\""