--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Tue Jul 21 12:51:14 2009 +0200
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Wed Jul 22 01:10:14 2009 +0200
@@ -62,20 +62,21 @@
   \<Longrightarrow> pred ts"}
   \end{isabelle}
   
-  For the purposes here, we will assume the @{text rules} have
-  this format and omit any code that actually tests this. Therefore ``things'' 
-  can go horribly wrong, if the @{text "rules"} are not of this
-  form.\footnote{FIXME: Exercise to test this format.} The @{text As} and
-  @{text Bs} in a @{text "rule"} stand for formulae not involving the inductive
-  predicates @{text "preds"}; the instances @{text "pred ss"} and @{text "pred
-  ts"} can stand for different predicates, like @{text "pred\<^isub>1 ss"} and 
-  @{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the
-  arguments of these predicates. Every formula left of @{text [quotes]
-  "\<Longrightarrow> pred ts"} is a premise of the rule. The outermost quantified 
-  variables @{text "xs"} are usually omitted in the user's input. The 
-  quantification for the variables @{text "ys"} is local with respect to 
-  one recursive premise and must be given. Some examples of @{text "rule"}s 
-  are
+  For the purposes here, we will assume the @{text rules} have this format and
+  omit any code that actually tests this. Therefore ``things'' can go horribly
+  wrong, if the @{text "rules"} are not of this form.\footnote{FIXME: Exercise
+  to test this format.} The @{text As} and @{text Bs} in a @{text "rule"}
+  stand for formulae not involving the inductive predicates @{text "preds"};
+  the instances @{text "pred ss"} and @{text "pred ts"} can stand for
+  different predicates, like @{text "pred\<^isub>1 ss"} and @{text
+  "pred\<^isub>2 ts"}, in case mutual recursive predicates are defined; the
+  terms @{text ss} and @{text ts} are the arguments of these predicates. Every
+  formula left of @{text [quotes] "\<Longrightarrow> pred ts"} is a premise of the rule. The
+  outermost quantified variables @{text "xs"} are usually omitted in the
+  user's input. The quantification for the variables @{text "ys"} is local
+  with respect to one recursive premise and must be given. Some examples of
+  @{text "rule"}s are
+
 
   @{thm [display] fresh_var[no_vars]}
 
@@ -159,10 +160,10 @@
   @{text [display] "pred ts"}
 
   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 
+  into the assumption. 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. After lifting to the meta-connectives, this introduction rule must necessarily 
-  be of the form 
+  proving. After transforming the object connectives into 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"}
 

Binary file progtutorial.pdf has changed