--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 13:27:12 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 13:46:53 2009 +0100
@@ -765,7 +765,7 @@
   The reason is that the theory and the name of the data type can easily change. 
   To make the code more robust, it is better to use the antiquotation 
   @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
-  variable parts of the constant's name. Therefore a functions for 
+  variable parts of the constant's name. Therefore a function for 
   matching against constants that have a polymorphic type should 
   be written as follows.
 *}
@@ -775,7 +775,7 @@
   | is_nil_or_all _ = false *}
 
 text {*
-  Occasional you have to calculate what the ``base'' name of a given
+  Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML Sign.extern_const} or
   @{ML Long_Name.base_name}. For example:
 
@@ -816,7 +816,7 @@
    | _ => t)*}
 
 text {*
-  An example as follows:
+  Here is an example:
 
 @{ML_response_fake [display,gray] 
 "map_types nat_to_int @{term \"a = (1::nat)\"}" 
@@ -885,7 +885,7 @@
   result that type-checks.
   \end{exercise}
 
-  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 type_of} returns the 
@@ -935,12 +935,12 @@
   Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
 
   Instead of giving explicitly the type for the constant @{text "plus"} and the free 
-  variable @{text "x"}, the type-inference fills in the missing information.
+  variable @{text "x"}, type-inference fills in the missing information.
 
   \begin{readmore}
   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
-  checking and pretty-printing of terms are defined. Functions related to the
-  type inference are implemented in @{ML_file "Pure/type.ML"} and 
+  checking and pretty-printing of terms are defined. Functions related to
+  type-inference are implemented in @{ML_file "Pure/type.ML"} and 
   @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
 

Binary file progtutorial.pdf has changed