# HG changeset patch
# User wenzelm
# Date 1005603978 -3600
# Node ID 0b219d9e3384b9943c7c099b67e8c4d0f5623a79
# Parent  04c98351f9af28f8e323a362fec46a0bd86e6b41
induct_atomize: include atomize_conj (for mutual induction);

diff -r 04c98351f9af -r 0b219d9e3384 src/FOL/FOL.thy
--- 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