# HG changeset patch
# User wenzelm
# Date 1013541958 -3600
# Node ID bda60442bf02a98a54b2ec67a4635d5da7d3c532
# Parent  368966ceafe5ad86b1235bdb6e3ff7aac447cfa3
tuned;

diff -r 368966ceafe5 -r bda60442bf02 src/FOL/IFOL.thy
--- 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)