src/FOL/IFOL.thy
 changeset 12937 0c4fd7529467 parent 12875 bda60442bf02 child 13435 05631e8f0258
```     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)
```