Fixed problem with induct_conj_curry: variable C should have type prop.

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)