--- a/ProgTutorial/General.thy	Sun Oct 18 08:44:39 2009 +0200
+++ b/ProgTutorial/General.thy	Sun Oct 18 21:22:44 2009 +0200
@@ -16,7 +16,8 @@
 text {*
   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
+  everything else is build on top of this trusted core 
+  \cite{GordonMilnerWadsworth79}. The fundamental data
   structures involved in this core are certified terms and certified types, 
   as well as theorems.
 *}
@@ -720,7 +721,8 @@
   "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
   "P 3"}
 
-  Similarly @{ML_ind list_comb in Drule} applies a list of @{ML_type cterm}s.
+  Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule}
+  applies a list of @{ML_type cterm}s.
 
   @{ML_response_fake [display,gray]
   "let
@@ -743,8 +745,7 @@
 text {*
   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
   that can only be built by going through interfaces. As a consequence, every proof 
-  in Isabelle is correct by construction. This follows the tradition of the LCF approach
-  \cite{GordonMilnerWadsworth79}.
+  in Isabelle is correct by construction. This follows the tradition of the LCF approach.
 
 
   To see theorems in ``action'', let us give a proof on the ML-level for the following 
@@ -752,9 +753,9 @@
 *}
 
   lemma 
-   assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
-   and     assm\<^isub>2: "P t"
-   shows "Q t" (*<*)oops(*>*) 
+    assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
+    and     assm\<^isub>2: "P t"
+    shows "Q t"(*<*)oops(*>*) 
 
 text {*
   The corresponding ML-code is as follows:
@@ -803,7 +804,8 @@
   While we obtained a theorem as result, this theorem is not
   yet stored in Isabelle's theorem database. Consequently, it cannot be 
   referenced on the user level. One way to store it in the theorem database is
-  by using the function @{ML_ind note in LocalTheory}.
+  by using the function @{ML_ind note in LocalTheory}.\footnote{\bf FIXME: make sure a pointer
+  to the section about local-setup is given eralier.}
 *}
 
 local_setup %gray {*
@@ -814,12 +816,12 @@
   The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
   classifies the theorem. There are several such kind indicators: for a
   theorem arising from a definition we should use @{ML_ind definitionK in
-  Thm}, for an axiom @{ML_ind axiomK in Thm}, for ``normal'' theorems the
+  Thm}, for an axiom @{ML_ind axiomK in Thm}, and for ``normal'' theorems the
   kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK in Thm}.  The second
   argument of @{ML note in LocalTheory} is the name under which we store the
-  theorem or theorems. The third argument can contain a list of (theorem)
-  attributes. We will explain them in detail in
-  Section~\ref{sec:attributes}. Below we just use one such attribute in order add
+  theorem or theorems. The third argument can contain a list of theorem
+  attributes, which we will explain in detail in Section~\ref{sec:attributes}. 
+  Below we just use one such attribute in order add
   the theorem to the simpset:
 *}
 
@@ -830,7 +832,7 @@
 
 text {*
   Note that we have to use another name under which the theorem is stored,
-  since Isabelle does not allow us to store another theorem under the same
+  since Isabelle does not allow us to store two theorems under the same
   name. The attribute needs to be wrapped inside the function @{ML_ind
   internal in Attrib}. If we use the function @{ML get_thm_names_from_ss} from
   the previous chapter, we can check whether the theorem has actually been
@@ -855,16 +857,17 @@
    @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
   \end{isabelle}
 
-  or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen
+  or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen,
   the theorem does not have any meta-variables that would be present if we proved
-  this theorem on the user-level. We will see later on that usually we have to 
+  this theorem on the user-level. We will see later on that we have to 
   construct meta-variables in theorems explicitly.
 
   \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}}
 *}
 
 text {*
-  There is a multitude of functions that manage or manipulate theorems. For example 
+  There is a multitude of functions that manage or manipulate theorems in the 
+  structures @{ML_struct Thm} and @{ML_struct Drule}. For example 
   we can test theorems for alpha equality. Suppose you proved the following three 
   theorems.
 *}