1.1 --- a/src/FOL/IFOL.thy	Mon Feb 25 20:46:09 2002 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Mon Feb 25 20:48:14 2002 +0100
     1.3 @@ -126,7 +126,10 @@
     1.4  subsection {* Intuitionistic Reasoning *}
     1.5  
     1.6  lemma impE':
     1.7 -  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
     1.8 +  assumes 1: "P --> Q"
     1.9 +    and 2: "Q ==> R"
    1.10 +    and 3: "P --> Q ==> P"
    1.11 +  shows R
    1.12  proof -
    1.13    from 3 and 1 have P .
    1.14    with 1 have Q by (rule impE)
    1.15 @@ -134,13 +137,18 @@
    1.16  qed
    1.17  
    1.18  lemma allE':
    1.19 -  (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q
    1.20 +  assumes 1: "ALL x. P(x)"
    1.21 +    and 2: "P(x) ==> ALL x. P(x) ==> Q"
    1.22 +  shows Q
    1.23  proof -
    1.24    from 1 have "P(x)" by (rule spec)
    1.25    from this and 1 show Q by (rule 2)
    1.26  qed
    1.27  
    1.28 -lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
    1.29 +lemma notE':
    1.30 +  assumes 1: "~ P"
    1.31 +    and 2: "~ P ==> P"
    1.32 +  shows R
    1.33  proof -
    1.34    from 2 and 1 have P .
    1.35    with 1 show R by (rule notE)