1.1 --- a/src/FOL/IFOL.thy	Mon Feb 11 17:30:58 2002 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Tue Feb 12 20:25:58 2002 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4  use "intprover.ML"
     1.5  
     1.6  
     1.7 -subsubsection {* Intuitionistic Reasoning *}
     1.8 +subsection {* Intuitionistic Reasoning *}
     1.9  
    1.10  lemma impE':
    1.11    (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
    1.12 @@ -192,7 +192,8 @@
    1.13    thus "x == y" by (rule eq_reflection)
    1.14  qed
    1.15  
    1.16 -lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
    1.17 +lemma atomize_conj [atomize]:
    1.18 +  "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
    1.19  proof
    1.20    assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
    1.21    show "A & B" by (rule conjI)