--- a/ProgTutorial/Package/Ind_Prelims.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -9,14 +9,15 @@
   expects from the package to produce a convenient reasoning
   infrastructure. This infrastructure needs to be derived from the definition
   that correspond to the specified predicate(s). Before we start with
-  explaining all parts of the package, let us first give some examples 
-  showing how to define inductive predicates and then also how
-  to generate a reasoning infrastructure for them. From the examples 
-  we will figure out a general method for
-  defining inductive predicates.  The aim in this section is \emph{not} to
+  explaining all parts of the package, let us first give some examples showing
+  how to define inductive predicates and then also how to generate a reasoning
+  infrastructure for them. From the examples we will figure out a general
+  method for defining inductive predicates. This is usually the first step in
+  writing a package for Isabelle. The aim in this section is \emph{not} to
   write proofs that are as beautiful as possible, but as close as possible to
   the ML-implementation we will develop in later sections.
 
+
   We first consider the transitive closure of a relation @{text R}. The 
   ``pencil-and-paper'' specification for the transitive closure is:
 
@@ -25,12 +26,12 @@
   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
   \end{center}
 
-  The package has to make an appropriate definition for @{term "trcl"}. 
-  Since an inductively
-  defined predicate is the least predicate closed under a collection of
-  introduction rules, the predicate @{text "trcl R x y"} can be defined so
-  that it holds if and only if @{text "P x y"} holds for every predicate
-  @{text P} closed under the rules above. This gives rise to the definition
+  As mentioned before, the package has to make an appropriate definition for
+  @{term "trcl"}. Since an inductively defined predicate is the least
+  predicate closed under a collection of introduction rules, the predicate
+  @{text "trcl R x y"} can be defined so that it holds if and only if @{text
+  "P x y"} holds for every predicate @{text P} closed under the rules
+  above. This gives rise to the definition
 *}
 
 definition "trcl \<equiv> 
@@ -38,11 +39,11 @@
                   \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"
 
 text {*
-  We have to use the object implication @{text "\<longrightarrow>"} and object quantification
-  @{text "\<forall>"} for stating this definition (there is no other way for
-  definitions in HOL). However, the introduction rules and induction
-  principles associated with the transitive closure should use the meta-connectives, 
-  since they simplify the reasoning for the user.
+  Note we have to use the object implication @{text "\<longrightarrow>"} and object
+  quantification @{text "\<forall>"} for stating this definition (there is no other
+  way for definitions in HOL). However, the introduction rules and induction
+  principles associated with the transitive closure should use the
+  meta-connectives, since they simplify the reasoning for the user.
 
 
   With this definition, the proof of the induction principle for @{term trcl}
@@ -176,7 +177,7 @@
   declare new intro- or simplification rules that can throw automatic tactics
   off course) and also it is very hard to debug proofs involving automatic
   tactics whenever something goes wrong. Therefore if possible, automatic 
-  tactics should be avoided or be constrained sufficiently.
+  tactics in packages should be avoided or be constrained sufficiently.
 
   The method of defining inductive predicates by impredicative quantification
   also generalises to mutually inductive predicates. The next example defines
@@ -245,7 +246,7 @@
 qed
 
 text {*
-  The interesting lines are 7 to 15. The assumptions fall into two categories:
+  The interesting lines are 7 to 15. Again, the assumptions fall into two categories:
   @{text p1} corresponds to the premise of the introduction rule; @{text "r1"}
   to @{text "r3"} come from the definition of @{text "even"}.
   In Line 13, we apply the assumption @{text "r2"} (since we prove the second
@@ -262,6 +263,8 @@
   \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
   \end{center}
 
+  The interesting point of this definition is that it contains a quantification
+  that ranges only over the premise and the premise has also a precondition.
   The definition of @{text "accpart"} is:
 *}
 
@@ -294,7 +297,7 @@
 qed
 
 text {*
-  As you can see, there are now two subproofs. The assumptions fall again into
+  As you can see, there are now two subproofs. The assumptions fall as usual into
   two categories (Lines 7 to 9). In Line 11, applying the assumption @{text
   "r1"} generates a goal state with the new local assumption @{term "R y x"},
   named @{text "r1_prem"} in the second subproof (Line 14). This local assumption is