# HG changeset patch
# User wenzelm
# Date 1005592971 -3600
# Node ID ea4fbf26a9450e1832e1427ce792daf68bae8510
# Parent  a5cf3ea0685d458920d6c429246629a7686a6abe
lemmas induct_atomize = atomize_conj ...;
val local_imp_def = thm "induct_implies_def";

diff -r a5cf3ea0685d -r ea4fbf26a945 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Nov 12 20:22:23 2001 +0100
+++ b/src/HOL/HOL.thy	Mon Nov 12 20:22:51 2001 +0100
@@ -306,10 +306,9 @@
 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_rulify2 =
-  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
+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 induct_conj_def
 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
 
 hide const induct_forall induct_implies induct_equal induct_conj
@@ -322,6 +321,7 @@
   (struct
     val dest_concls = HOLogic.dest_concls;
     val cases_default = thm "case_split";
+    val local_imp_def = thm "induct_implies_def";
     val local_impI = thm "induct_impliesI";
     val conjI = thm "conjI";
     val atomize = thms "induct_atomize";