--- a/src/FOL/IFOL.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/FOL/IFOL.thy Mon Feb 25 20:48:14 2002 +0100
@@ -126,7 +126,10 @@
subsection {* Intuitionistic Reasoning *}
lemma impE':
- (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
+ assumes 1: "P --> Q"
+ and 2: "Q ==> R"
+ and 3: "P --> Q ==> P"
+ shows R
proof -
from 3 and 1 have P .
with 1 have Q by (rule impE)
@@ -134,13 +137,18 @@
qed
lemma allE':
- (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q
+ assumes 1: "ALL x. P(x)"
+ and 2: "P(x) ==> ALL x. P(x) ==> Q"
+ shows Q
proof -
from 1 have "P(x)" by (rule spec)
from this and 1 show Q by (rule 2)
qed
-lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
+lemma notE':
+ assumes 1: "~ P"
+ and 2: "~ P ==> P"
+ shows R
proof -
from 2 and 1 have P .
with 1 show R by (rule notE)