# HG changeset patch
# User wenzelm
# Date 1004133553 -7200
# Node ID f98623fdf6ef406f6625eb3fa4d05bbf9cd3feb3
# Parent  b10f1e8862f4000baa1f193abbb3ba633be46f6b
atomize_conj;

diff -r b10f1e8862f4 -r f98623fdf6ef src/FOL/IFOL.thy
--- 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]
 
 
diff -r b10f1e8862f4 -r f98623fdf6ef src/HOL/HOL.thy
--- 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 *}