# HG changeset patch
# User berghofe
# Date 1033394945 -7200
# Node ID 8bc77b17f59ffca0f5253ecb64478154d0b40794
# Parent  a8230e035e96c5363b409ee3e00708f1ddd59967
Fixed problem with induct_conj_curry: variable C should have type prop.

diff -r a8230e035e96 -r 8bc77b17f59f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Sep 30 15:45:11 2002 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 30 16:09:05 2002 +0200
@@ -549,8 +549,14 @@
     induct_conj (induct_implies C A) (induct_implies C B)"
   by (unfold induct_implies_def induct_conj_def) rules
 
-lemma induct_conj_curry: "(induct_conj A B ==> C) == (A ==> B ==> C)"
-  by (simp only: atomize_imp atomize_eq induct_conj_def) (rules intro: equal_intr_rule)
+lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
+proof
+  assume r: "induct_conj A B ==> PROP C" and A B
+  show "PROP C" by (rule r) (simp! add: induct_conj_def)
+next
+  assume r: "A ==> B ==> PROP C" and "induct_conj A B"
+  show "PROP C" by (rule r) (simp! add: induct_conj_def)+
+qed
 
 lemma induct_impliesI: "(A ==> B) ==> induct_implies A B"
   by (simp add: induct_implies_def)