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