--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Mon Mar 30 09:33:50 2009 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Tue Mar 31 15:48:53 2009 +0100
@@ -70,13 +70,11 @@
   has a single recursive premise that has a precondition. As usual all 
   rules are stated without the leading meta-quantification @{text "\<And>xs"}.
 
-  The code of the inductive package falls roughly in tree parts: the first
-  deals with the definitions, the second with the induction principles and 
-  the third with the introduction rules. 
-  
-  For the definitions we need to have the @{text rules} in a form where 
-  the meta-quantifiers and meta-implications are replaced by their object 
-  logic equivalents. Therefore an @{text "orule"} is of the form 
+  The output of the inductive package will be definitions for the predicates, 
+  induction principles and introduction rules.  For the definitions we need to have the
+  @{text rules} in a form where the meta-quantifiers and meta-implications are
+  replaced by their object logic equivalents. Therefore an @{text "orule"} is
+  of the form
 
   @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
 
@@ -111,13 +109,13 @@
   with the @{text "Ps"}. Then we are done since we are left with a simple 
   identity.
   
-  Although the user declares introduction rules @{text rules}, they must 
+  Although the user declares the introduction rules @{text rules}, they must 
   also be derived from the @{text defs}. These derivations are a bit involved. 
   Assuming we want to prove the introduction rule 
 
   @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
-  then we can have assumptions of the form
+  then we have assumptions of the form
 
   \begin{isabelle}
   (i)~~@{text "As"}\\
@@ -143,7 +141,8 @@
   In the last step we removed some quantifiers and moved the precondition @{text "orules"}  
   into the assumtion. The @{text "orules"} stand for all introduction rules that are given 
   by the user. We apply the @{text orule} that corresponds to introduction rule we are 
-  proving. This introduction rule must necessarily be of the form 
+  proving. After lifting to the meta-connectives, this introduction rule must necessarily 
+  be of the form 
 
   @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
@@ -167,10 +166,10 @@
   in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after.
   This completes the proof for introduction rules.
 
-  What remains is to implement the reasoning outlined in this section. We do this  
-  next. For building testcases, we use the shorthands for 
+  What remains is to implement in Isabelle the reasoning outlined in this section. 
+  We will describe the code in the next section. For building testcases, we use the shorthands for 
   @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}
-  given in Figure~\ref{fig:shorthands}.
+  defined in Figure~\ref{fig:shorthands}.
 *}