--- a/CookBook/Package/Simple_Inductive_Package.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Package/Simple_Inductive_Package.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -31,7 +31,7 @@
 simple_inductive
   accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
-  accpartI: "(\<forall>y. r y x \<longrightarrow> accpart r y) \<Longrightarrow> accpart r x"
+  accpartI: "(\<And>y. r y x \<Longrightarrow> accpart r y) \<Longrightarrow> accpart r x"
 
 thm accpart_def
 thm accpart.induct
@@ -53,9 +53,6 @@
 
 thm rel.accpartI'
 thm rel.accpart'.induct
-
-
-lemma "True" by simp
 *)
 
 use_chunks "simple_inductive_package.ML"