src/HOL/HOL.thy
changeset 13598 8bc77b17f59f
parent 13596 ee5f79b210c1
child 13638 2b234b079245
     1.1 --- a/src/HOL/HOL.thy	Mon Sep 30 15:45:11 2002 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 30 16:09:05 2002 +0200
     1.3 @@ -549,8 +549,14 @@
     1.4      induct_conj (induct_implies C A) (induct_implies C B)"
     1.5    by (unfold induct_implies_def induct_conj_def) rules
     1.6  
     1.7 -lemma induct_conj_curry: "(induct_conj A B ==> C) == (A ==> B ==> C)"
     1.8 -  by (simp only: atomize_imp atomize_eq induct_conj_def) (rules intro: equal_intr_rule)
     1.9 +lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
    1.10 +proof
    1.11 +  assume r: "induct_conj A B ==> PROP C" and A B
    1.12 +  show "PROP C" by (rule r) (simp! add: induct_conj_def)
    1.13 +next
    1.14 +  assume r: "A ==> B ==> PROP C" and "induct_conj A B"
    1.15 +  show "PROP C" by (rule r) (simp! add: induct_conj_def)+
    1.16 +qed
    1.17  
    1.18  lemma induct_impliesI: "(A ==> B) ==> induct_implies A B"
    1.19    by (simp add: induct_implies_def)