--- a/src/FOL/FOL.thy Mon Nov 12 23:25:25 2001 +0100
+++ b/src/FOL/FOL.thy Mon Nov 12 23:26:18 2001 +0100
@@ -61,8 +61,8 @@
lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)"
by (simp add: induct_implies_def)
-lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq
-lemmas induct_rulify1 = induct_atomize [symmetric, standard]
+lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq
+lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq
lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
hide const induct_forall induct_implies induct_equal