--- a/src/FOL/IFOL.thy Mon Feb 11 17:30:58 2002 +0100
+++ b/src/FOL/IFOL.thy Tue Feb 12 20:25:58 2002 +0100
@@ -123,7 +123,7 @@
use "intprover.ML"
-subsubsection {* Intuitionistic Reasoning *}
+subsection {* Intuitionistic Reasoning *}
lemma impE':
(assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
@@ -192,7 +192,8 @@
thus "x == y" by (rule eq_reflection)
qed
-lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
+lemma atomize_conj [atomize]:
+ "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
proof
assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
show "A & B" by (rule conjI)