--- a/src/FOL/IFOL.thy Fri Oct 26 23:58:21 2001 +0200
+++ b/src/FOL/IFOL.thy Fri Oct 26 23:59:13 2001 +0200
@@ -158,6 +158,21 @@
thus "x == y" by (rule eq_reflection)
qed
+lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
+proof (rule equal_intr_rule)
+ assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
+ show "A & B" by (rule conjI)
+next
+ fix C
+ assume "A & B"
+ assume "A ==> B ==> PROP C"
+ thus "PROP C"
+ proof this
+ show A by (rule conjunct1)
+ show B by (rule conjunct2)
+ qed
+qed
+
declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify]
--- a/src/HOL/HOL.thy Fri Oct 26 23:58:21 2001 +0200
+++ b/src/HOL/HOL.thy Fri Oct 26 23:59:13 2001 +0200
@@ -232,6 +232,21 @@
thus "x == y" by (rule eq_reflection)
qed
+lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
+proof (rule equal_intr_rule)
+ assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
+ show "A & B" by (rule conjI)
+next
+ fix C
+ assume "A & B"
+ assume "A ==> B ==> PROP C"
+ thus "PROP C"
+ proof this
+ show A by (rule conjunct1)
+ show B by (rule conjunct2)
+ qed
+qed
+
subsubsection {* Classical Reasoner setup *}