src/HOL/HOL.thy
changeset 12161 ea4fbf26a945
parent 12114 a8e860c86252
child 12240 0760eda193c4
     1.1 --- a/src/HOL/HOL.thy	Mon Nov 12 20:22:23 2001 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Nov 12 20:22:51 2001 +0100
     1.3 @@ -306,10 +306,9 @@
     1.4  lemma induct_impliesI: "(A ==> B) ==> induct_implies A B"
     1.5    by (simp add: induct_implies_def)
     1.6  
     1.7 -lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq
     1.8 -lemmas induct_rulify1 = induct_atomize [symmetric, standard]
     1.9 -lemmas induct_rulify2 =
    1.10 -  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.11 +lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq
    1.12 +lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq
    1.13 +lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.14  lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
    1.15  
    1.16  hide const induct_forall induct_implies induct_equal induct_conj
    1.17 @@ -322,6 +321,7 @@
    1.18    (struct
    1.19      val dest_concls = HOLogic.dest_concls;
    1.20      val cases_default = thm "case_split";
    1.21 +    val local_imp_def = thm "induct_implies_def";
    1.22      val local_impI = thm "induct_impliesI";
    1.23      val conjI = thm "conjI";
    1.24      val atomize = thms "induct_atomize";