
diff -r 83d5bca38bec -r 4c54ef4dc84d ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Sun Oct 11 23:16:34 2009 +0200
+++ b/ProgTutorial/General.thy	Mon Oct 12 17:07:17 2009 +0200
@@ -5,18 +5,19 @@
 chapter {* Let's Talk About the Good, the Bad and the Ugly *}
 
 text {*
-  Isabelle is build around a few central ideas. One 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 central data structures involved
-  in this core are certified terms and types as well as theorems.
+  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.
 *}
 
 
 section {* Terms and Types *}
 
 text {*
-  In Isabelle there are certified terms (respectively types) and uncertified
-  terms. The latter are called just terms. One way to construct them is by 
+  There are certified terms and uncertified terms (respectively types). 
+  Uncertified terms are just called terms. One way to construct them is by 
   using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
 
   @{ML_response [display,gray] 
@@ -24,8 +25,8 @@
 "Const (\"op =\", \<dots>) $ 
   (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
-  will show the term @{term "(a::nat) + b = c"}, but printed using the internal
-  representation corresponding to the datatype @{ML_type  "term"} defined as follows: 
+  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: 
 *}  
 
 ML_val %linenosgray{*datatype term =
@@ -37,10 +38,10 @@
 | $ of term * term *}
 
 text {*
-  This datatype implements lambda-terms typed in Church-style.
-  As can be seen in Line 5, terms use the usual de Bruijn index mechanism
-  for representing bound variables.  For
-  example in
+  This datatype implements Church-style lambda-terms, where types are
+  explicitly recorded in the 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
 
   @{ML_response_fake [display, gray]
   "@{term \"\<lambda>x y. x y\"}"
@@ -75,7 +76,7 @@
   mentioned earlier, you cannot construct schematic variables using the
   antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,
   however, observe the distinction. The reason is that only schematic
-  varaibles can be instantiated with terms when a theorem is applied. A
+  variables can be instantiated with terms when a theorem is applied. A
   similar distinction between free and schematic variables holds for types
   (see below).
 
@@ -97,7 +98,7 @@
 
   @{ML_response_fake [display,gray] 
 "let
-  val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
+  val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
 in 
   tracing (string_of_term @{context} omega)
 end"
@@ -224,10 +225,11 @@
     Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
-  There are a number of handy functions that are frequently used for 
-  constructing terms. One is the function @{ML_ind  list_comb}, which takes a term
-  and a list of terms as arguments, and produces as output the term
-  list applied to the term. For example
+  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
+  term list applied to the term. For example
+
 
 @{ML_response_fake [display,gray]
 "let
@@ -238,7 +240,7 @@
 end"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 
-  Another handy function is @{ML_ind  lambda}, which abstracts a variable 
+  Another handy function is @{ML_ind lambda in Term}, which abstracts a variable 
   in a term. For example
 
   @{ML_response_fake [display,gray]
@@ -271,7 +273,7 @@
   of Church-style typing, where variables with the same name still differ, if they 
   have different type.
 
-  There is also the function @{ML_ind  subst_free} with which terms can be
+  There is also the function @{ML_ind subst_free in Term} with which terms can be
   replaced by other terms. For example below, we will replace in @{term
   "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
   @{term y}, and @{term x} by @{term True}.
@@ -298,13 +300,13 @@
 end"
   "Free (\"x\", \"nat\")"}
 
-  Similarly the function @{ML_ind  subst_bounds}, replaces lose bound 
+  Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound 
   variables with terms. To see how this function works, let us implement a
   function that strips off the outermost quantifiers in a term.
 *}
 
 ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =
-         strip_alls t |>> cons (Free (n, T))
+                                    strip_alls t |>> cons (Free (n, T))
   | strip_alls t = ([], t) *}
 
 text {*
@@ -318,7 +320,7 @@
 
   After calling @{ML strip_alls}, you obtain a term with lose bound variables. With
   the function @{ML subst_bounds}, you can replace these lose @{ML_ind 
-  Bound}s with the stripped off variables.
+  Bound in Term}s with the stripped off variables.
 
   @{ML_response_fake [display, gray, linenos]
   "let
@@ -336,7 +338,7 @@
   and so on. 
 
   There are many convenient functions that construct specific HOL-terms. For
-  example @{ML_ind  mk_eq in HOLogic} constructs an equality out of two terms.
+  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
 
@@ -451,7 +453,7 @@
   section and link with the comment in the antiquotation section.}
 
   Occasionally you have to calculate what the ``base'' name of a given
-  constant is. For this you can use the function @{ML_ind  "Sign.extern_const"} or
+  constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or
   @{ML_ind  Long_Name.base_name}. For example:
 
   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
@@ -474,13 +476,13 @@
 
 ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
 
-text {* This can be equally written with the combinator @{ML_ind  "-->"} as: *}
+text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *}
 
 ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
 
 text {*
   If you want to construct a function type with more than one argument
-  type, then you can use @{ML_ind  "--->"}.
+  type, then you can use @{ML_ind "--->" in Term}.
 *}
 
 ML{*fun make_fun_types tys ty = tys ---> ty *}
@@ -607,7 +609,7 @@
   Sometimes it is a bit inconvenient to construct a term with 
   complete typing annotations, especially in cases where the typing 
   information is redundant. A short-cut is to use the ``place-holder'' 
-  type @{ML_ind  dummyT} and then let type-inference figure out the 
+  type @{ML_ind dummyT in Term} and then let type-inference figure out the 
   complete type. An example is as follows:
 
   @{ML_response_fake [display,gray] 




