induct_impliesI;
authorwenzelm
Wed Oct 31 01:19:58 2001 +0100 (2001-10-31)
changeset 119888340fb172607
parent 11987 bf31b35949ce
child 11989 d4bcba4e080e
induct_impliesI;
src/FOL/FOL.thy
     1.1 --- a/src/FOL/FOL.thy	Tue Oct 30 17:37:25 2001 +0100
     1.2 +++ b/src/FOL/FOL.thy	Wed Oct 31 01:19:58 2001 +0100
     1.3 @@ -58,6 +58,9 @@
     1.4  lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
     1.5    by (simp only: atomize_eq induct_equal_def)
     1.6  
     1.7 +lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)"
     1.8 +  by (simp add: induct_implies_def)
     1.9 +
    1.10  lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq
    1.11  lemmas induct_rulify1 = induct_atomize [symmetric, standard]
    1.12  lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
    1.13 @@ -72,6 +75,7 @@
    1.14    (struct
    1.15      val dest_concls = FOLogic.dest_concls;
    1.16      val cases_default = thm "case_split";
    1.17 +    val local_impI = thm "induct_impliesI";
    1.18      val conjI = thm "conjI";
    1.19      val atomize = thms "induct_atomize";
    1.20      val rulify1 = thms "induct_rulify1";