# 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