--- a/CookBook/Package/Ind_Prelims.thy	Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/Package/Ind_Prelims.thy	Wed Mar 11 01:43:28 2009 +0000
@@ -75,10 +75,10 @@
 *}
 
 lemma %linenos trcl_induct:
-  assumes asm: "trcl R x y"
+  assumes "trcl R x y"
   shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
 apply(atomize (full))
-apply(cut_tac asm)
+apply(cut_tac prems)
 apply(unfold trcl_def)
 apply(drule spec[where x=P])
 apply(assumption)
@@ -212,11 +212,11 @@
 *}
 
 simple_inductive
-  even\<iota> and odd\<iota>
+  even and odd
 where
-  even0: "even\<iota> 0"
-| evenS: "odd\<iota> n \<Longrightarrow> even\<iota> (Suc n)"
-| oddS: "even\<iota> n \<Longrightarrow> odd\<iota> (Suc n)"
+  even0: "even 0"
+| evenS: "odd n \<Longrightarrow> even (Suc n)"
+| oddS: "even n \<Longrightarrow> odd (Suc n)"
 
 text {*
   Since the predicates @{term even} and @{term odd} are mutually inductive, each 
@@ -224,11 +224,11 @@
   below @{text "P"} and @{text "Q"}).
 *}
 
-definition "even \<equiv> 
+definition "even\<iota> \<equiv> 
   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
                  \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
 
-definition "odd \<equiv>
+definition "odd\<iota> \<equiv>
   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
                  \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
 
@@ -238,11 +238,11 @@
 *}
 
 lemma even_induct:
-  assumes asm: "even n"
+  assumes "even n"
   shows "P 0 \<Longrightarrow> 
              (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
 apply(atomize (full))
-apply(cut_tac asm)
+apply(cut_tac prems)
 apply(unfold even_def)
 apply(drule spec[where x=P])
 apply(drule spec[where x=Q])
@@ -263,7 +263,7 @@
 apply (unfold odd_def even_def)
 apply (rule allI impI)+
 proof -
-  case (goal1 P)
+  case (goal1 P Q)
   have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
                              \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
   have r1: "P 0" by fact
@@ -303,10 +303,10 @@
 *}
 
 lemma accpart_induct:
-  assumes asm: "accpart R x"
+  assumes "accpart R x"
   shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
 apply(atomize (full))
-apply(cut_tac asm)
+apply(cut_tac prems)
 apply(unfold accpart_def)
 apply(drule spec[where x=P])
 apply(assumption)