--- a/ProgTutorial/General.thy	Wed Oct 14 14:56:19 2009 +0200
+++ b/ProgTutorial/General.thy	Sun Oct 18 08:44:39 2009 +0200
@@ -17,16 +17,16 @@
   Isabelle is build around a few central ideas. One central idea is the
   LCF-approach to theorem proving where there is a small trusted core and
   everything else is build on top of this trusted core. The fundamental data
-  structures involved in this core are certified terms and types, as well as
-  theorems.
+  structures involved in this core are certified terms and certified types, 
+  as well as theorems.
 *}
 
 
 section {* Terms and Types *}
 
 text {*
-  There are certified terms and uncertified terms (respectively types). 
-  Uncertified terms are just called terms. One way to construct them is by 
+  In Isabelle, there are certified terms and uncertified terms (respectively types). 
+  Uncertified terms are often just called terms. One way to construct them is by 
   using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
 
   @{ML_response [display,gray] 
@@ -34,8 +34,9 @@
 "Const (\"op =\", \<dots>) $ 
   (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
-  constructs the term @{term "(a::nat) + b = c"}, but it printed using the internal
-  representation corresponding to the datatype @{ML_type_ind "term"} defined as follows: 
+  constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 
+  the internal representation corresponding to the datatype @{ML_type_ind "term"}, 
+  which is defined as follows: 
 *}  
 
 ML_val %linenosgray{*datatype term =
@@ -48,7 +49,7 @@
 
 text {*
   This datatype implements Church-style lambda-terms, where types are
-  explicitly recorded in the variables, constants and abstractions.  As can be
+  explicitly recorded in variables, constants and abstractions.  As can be
   seen in Line 5, terms use the usual de Bruijn index mechanism for
   representing bound variables.  For example in
 
@@ -153,7 +154,7 @@
 
   where it is not (since it is already constructed by a meta-implication). 
   The purpose of the @{text "Trueprop"}-coercion is to embed formulae of
-  an object logic, for example HOL, into the meta-logic of Isabelle. It
+  an object logic, for example HOL, into the meta-logic of Isabelle. The coercion
   is needed whenever a term is constructed that will be proved as a theorem. 
 
   As already seen above, types can be constructed using the antiquotation 
@@ -171,7 +172,7 @@
 
 text {*
   Like with terms, there is the distinction between free type
-  variables (term-constructor @{ML "TFree"} and schematic
+  variables (term-constructor @{ML "TFree"}) and schematic
   type variables (term-constructor @{ML "TVar"}). A type constant,
   like @{typ "int"} or @{typ bool}, are types with an empty list
   of argument types. However, it is a bit difficult to show an
@@ -236,7 +237,7 @@
 
   There are a number of handy functions that are frequently used for
   constructing terms. One is the function @{ML_ind list_comb in Term}, which
-  takes a term and a list of terms as arguments, and produces as output the
+  takes as argument a term and a list of terms, and produces as output the
   term list applied to the term. For example
 
 
@@ -262,7 +263,7 @@
   "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
   In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
-  and an abstraction. It also records the type of the abstracted
+  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"}
   is of the same type as the abstracted variable. If it is of different type,
@@ -320,7 +321,7 @@
 
 text {*
   The function returns a pair consisting of the stripped off variables and
-  the body of the universal quantifications. For example
+  the body of the universal quantification. For example
 
   @{ML_response_fake [display, gray]
   "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
@@ -346,7 +347,8 @@
   takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}
   and so on. 
 
-  There are many convenient functions that construct specific HOL-terms. For
+  There are also many convenient functions that construct specific HOL-terms
+  in the structure @{ML_struct HOLogic}. For
   example @{ML_ind mk_eq in HOLogic} constructs an equality out of two terms.
   The types needed in this equality are calculated from the type of the
   arguments. For example
@@ -545,14 +547,13 @@
   \end{exercise}
 
   \begin{exercise}\label{fun:makesum}
-  Write a function which takes two terms representing natural numbers
+  Write a function that takes two terms representing natural numbers
   in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
   number representing their sum.
   \end{exercise}
 
   \begin{exercise}\label{ex:debruijn}
-  Implement the function, which we below name deBruijn\footnote{According to 
-  personal communication of de Bruijn to Dyckhoff.}, that depends on a natural
+  Implement the function, which we below name deBruijn, that depends on a natural
   number n$>$0 and constructs terms of the form:
   
   \begin{center}
@@ -575,7 +576,8 @@
   \end{center}
 
   Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}
-  for constructing the terms for the logical connectives. 
+  for constructing the terms for the logical connectives.\footnote{Thanks to Roy
+  Dyckhoff for this exercise.} 
   \end{exercise}
 *}
 
@@ -1382,7 +1384,7 @@
   the current simpset.
 *}
 
-section {* Theories (TBD) *}
+section {* Theories\label{sec:theories} (TBD) *}
 
 text {*
   There are theories, proof contexts and local theories (in this order, if you