--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 12:13:21 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 12:35:15 2009 +0100
@@ -532,7 +532,7 @@
 section {* Terms and Types *}
 
 text {*
-  One way to construct terms of Isabelle is by using the antiquotation 
+  One way to construct Isabelle terms, is by using the antiquotation 
   \mbox{@{text "@{term \<dots>}"}}. For example:
 
   @{ML_response [display,gray] 
@@ -540,16 +540,16 @@
 "Const (\"op =\", \<dots>) $ 
   (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
-  This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
-  representation of this term. This internal representation corresponds to the 
-  datatype @{ML_type "term"}.
+  will show the term @{term "(a::nat) + b = c"}, but printed using an internal
+  representation corresponding to the datatype @{ML_type "term"}.
   
-  The internal representation of terms uses the usual de Bruijn index mechanism where bound 
-  variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
-  the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
-  binds the corresponding variable. However, in Isabelle the names of bound variables are 
-  kept at abstractions for printing purposes, and so should be treated only as ``comments''. 
-  Application in Isabelle is realised with the term-constructor @{ML $}.
+  This internal representation uses the usual de Bruijn index mechanism---where
+  bound variables are represented by the constructor @{ML Bound}.  The index in
+  @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip
+  until we hit the @{ML Abs} that binds the corresponding variable. Note that
+  the names of bound variables are kept at abstractions for printing purposes,
+  and so should be treated only as ``comments''.  Application in Isabelle is
+  realised with the term-constructor @{ML $}.
 
   \begin{readmore}
   Terms are described in detail in \isccite{sec:terms}. Their
@@ -885,7 +885,7 @@
   result that type-checks.
   \end{exercise}
 
-  Remember Isabelle foolows 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 
@@ -895,7 +895,7 @@
   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 
   To calculate the type, this function traverses the whole term and will
-  detect any typing inconsistency. For examle changing the type of the variable 
+  detect any typing inconsistency. For example changing the type of the variable 
   @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 
 
   @{ML_response_fake [display,gray] 
@@ -935,11 +935,11 @@
   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 filles in the missing information.
+  variable @{text "x"}, the 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. Fuctions related to the
+  checking and pretty-printing of terms are defined. Functions related to the
   type inference are implemented in @{ML_file "Pure/type.ML"} and 
   @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
@@ -1021,8 +1021,8 @@
   annotated to theorems, but functions that do further processing once a
   theorem is proven. In particular, it is not possible to find out
   what are all theorems that have a given attribute in common, unless of course
-  the function behind the attribute stores the theorems in a retrivable 
-  datastructure. 
+  the function behind the attribute stores the theorems in a retrievable 
+  data structure. 
 
   If you want to print out all currently known attributes a theorem 
   can have, you can use the function: