--- a/ProgTutorial/Essential.thy	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/Essential.thy	Wed Oct 15 23:12:54 2014 +0100
@@ -127,7 +127,7 @@
 
   When constructing terms, you are usually concerned with free
   variables (as mentioned earlier, you cannot construct schematic
-  variables using the built in antiquotation \mbox{@{text "@{term
+  variables using the built-in antiquotation \mbox{@{text "@{term
   \<dots>}"}}). If you deal with theorems, you have to, however, observe the
   distinction. The reason is that only schematic variables can be
   instantiated with terms when a theorem is applied. A similar
@@ -148,7 +148,7 @@
   "@{term \"x x\"}"
   "Type unification failed: Occurs check!"}
 
-  raises a typing error, while it perfectly ok to construct the term
+  raises a typing error, while it is perfectly ok to construct the term
   with the raw ML-constructors:
 
   @{ML_response_fake [display,gray] 
@@ -276,7 +276,7 @@
   that it is defined in the theory @{text "List"}. However, one has to be 
   careful with names of types, because even if
   @{text "fun"} is defined in the theory @{text "HOL"}, it is  
-  still represented by their simple name.
+  still represented by its simple name.
 
    @{ML_response [display,gray]
   "@{typ \"bool \<Rightarrow> nat\"}"
@@ -379,7 +379,7 @@
 end"
   "Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
-  In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
+  In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML "Bound 0"}), 
   and an abstraction, where it also records the type of the abstracted
   variable and for printing purposes also its name.  Note that because of the
   typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
@@ -792,7 +792,7 @@
   The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
   environment, which is needed for starting the unification without any
   (pre)instantiations. The @{text 0} is an integer index that will be explained
-  below. In case of failure, @{ML typ_unify in Sign} will throw the exception
+  below. In case of failure, @{ML typ_unify in Sign} will raise the exception
   @{text TUNIFY}.  We can print out the resulting type environment bound to 
   @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
   structure @{ML_struct Vartab}.
@@ -1123,7 +1123,7 @@
 
   As mentioned before, unrestricted higher-order unification, respectively
   unrestricted higher-order matching, is in general undecidable and might also
-  not posses a single most general solution. Therefore Isabelle implements the
+  not possess a single most general solution. Therefore Isabelle implements the
   unification function @{ML_ind unifiers in Unify} so that it returns a lazy
   list of potentially infinite unifiers.  An example is as follows
 *}
@@ -1200,7 +1200,7 @@
   problem can be solved by first-order matching.
 
   Higher-order matching might be necessary for instantiating a theorem
-  appropriately. More on this will be given in Sections~\ref{sec:theorems}. 
+  appropriately. More on this will be given in Section~\ref{sec:theorems}. 
   Here we only have a look at a simple case, namely the theorem 
   @{thm [source] spec}:
 
@@ -1212,7 +1212,7 @@
   as an introduction rule. Applying it directly can lead to unexpected
   behaviour since the unification has more than one solution. One way round
   this problem is to instantiate the schematic variables @{text "?P"} and
-  @{text "?x"}.  instantiation function for theorems is 
+  @{text "?x"}.  Instantiation function for theorems is 
   @{ML_ind instantiate_normalize in Drule} from the structure 
   @{ML_struct Drule}. One problem, however, is
   that this function expects the instantiations as lists of @{ML_type ctyp}
@@ -1309,10 +1309,10 @@
   Overloading a constant means specifying its value on a type based on
   a well-founded reduction towards other values of constants on types.
   When instantiating type classes
-  (i.e. proving arities) you are specifying overloading via primitive recursion.
+  (i.e.\ proving arities) you are specifying overloading via primitive recursion.
 
   Sorts are finite intersections of type classes and are implemented as lists
-  of type class names. The empty intersection, i.e. the empty list, is therefore
+  of type class names. The empty intersection, i.e.\ the empty list, is therefore
   inhabited by all types and is called the topsort.
 
   Free and schematic type variables are always annotated with sorts, thereby restricting
@@ -1348,7 +1348,7 @@
 section {* Type-Checking\label{sec:typechecking} *}
 
 text {* 
-  Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 
+  Remember Isabelle follows the Church-style typing for terms, i.e.\ a term contains 
   enough typing information (constants, free variables and abstractions all have typing 
   information) so that it is always clear what the type of a term is. 
   Given a well-typed term, the function @{ML_ind type_of in Term} returns the