src/HOL/Isar_examples/Peirce.thy

--- a/src/HOL/Isar_examples/Peirce.thy	Fri Sep 03 14:21:59 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Fri Sep 03 14:22:12 1999 +0200
@@ -12,15 +12,13 @@
   assume aba: "(A --> B) --> A";
   show A;
   proof (rule classical);
-    assume not_a: "~ A";
-
-    have ab: "A --> B";
+    assume "~ A";
+    have "A --> B";
     proof;
-      assume a: A;
-      show B; by contradiction;
+      assume A;
+      thus B; by contradiction;
     qed;
-
-    from aba ab; show A; ..;
+    with aba; show A; ..;
   qed;
 qed;
 
@@ -30,14 +28,14 @@
   assume aba: "(A --> B) --> A";
   show A;
   proof (rule classical);
-    presume ab: "A --> B";
-    from aba ab; show A; ..;
+    presume "A --> B";
+    with aba; show A; ..;
   next;
     assume not_a: "~ A";
     show "A --> B";
     proof;
-      assume a: A;
-      from not_a a; show B; ..;
+      assume A;
+      with not_a; show B; ..;
     qed;
   qed;
 qed;