--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -41,9 +41,9 @@
 
 text {*
   The inductive package will generate the reasoning infrastructure for
-  mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
+  mutually recursive predicates, say @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
   follows we will have the convention that various, possibly empty collections
-  of ``things'' (lists, nested implications and so on) are indicated either by
+  of ``things'' (lists, terms, nested implications and so on) are indicated either by
   adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes]
   "\<^isup>*"}. The shorthand for the predicates will therefore be @{text
   "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must
@@ -64,18 +64,17 @@
   
   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
+  wrong, if the @{text "rules"} are not of this form.  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]}
@@ -88,7 +87,7 @@
 
   @{thm [display] accpartI[no_vars]}
 
-  has a single recursive premise that has a precondition. As usual all 
+  has a single recursive premise that has a precondition. As is custom all 
   rules are stated without the leading meta-quantification @{text "\<And>xs"}.
 
   The output of the inductive package will be definitions for the predicates, 
@@ -108,7 +107,7 @@
 
   @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
 
-  where in the @{text "rules"} every @{text pred} is replaced by a fresh
+  where in the @{text "rules"}-part every @{text pred} is replaced by a fresh
   meta-variable @{text "?P"}.
 
   In order to derive an induction principle for the predicate @{text "pred"},
@@ -211,11 +210,11 @@
    @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},
    @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]
 
-val eo_preds =  [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] 
+val eo_preds =  [@{term "even::nat \<Rightarrow> bool"}, @{term "odd::nat \<Rightarrow> bool"}] 
 val eo_prednames = [@{binding "even"}, @{binding "odd"}]
 val eo_mxs = [NoSyn, NoSyn] 
 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] 
-val e_pred = @{term "even::nat\<Rightarrow>bool"}
+val e_pred = @{term "even::nat \<Rightarrow> bool"}
 val e_arg_tys = [@{typ "nat"}] 
 
 
@@ -233,7 +232,7 @@
    @{prop "\<forall>a t. fresh a (Lam a t)"},
    @{prop "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}]
 
-val fresh_pred =  @{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"} 
+val fresh_pred =  @{term "fresh::string \<Rightarrow> trm \<Rightarrow> bool"} 
 val fresh_arg_tys = [@{typ "string"}, @{typ "trm"}]
 
 
@@ -241,11 +240,11 @@
 (* accessible-part example *)
 val acc_rules = 
      [@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}]
-val acc_pred = @{term "accpart::('a \<Rightarrow>'a\<Rightarrow>bool)\<Rightarrow>'a \<Rightarrow>bool"}*}
+val acc_pred = @{term "accpart::('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a \<Rightarrow> bool"}*}
 text_raw{*
 \end{isabelle}
 \end{minipage}
-\caption{Shorthands for the inductive predicates @{text "even"}-@{text "odd"}, 
+\caption{Shorthands for the inductive predicates @{text "even"}/@{text "odd"}, 
   @{text "fresh"} and @{text "accpart"}. The names of these shorthands follow 
   the convention @{text "rules"}, @{text "orules"}, @{text "preds"} and so on. 
   The purpose of these shorthands is to simplify the construction of testcases