tuned;

--- a/src/HOL/Isar_examples/MultisetOrder.thy	Fri Sep 03 14:21:59 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Fri Sep 03 14:22:12 1999 +0200
@@ -36,10 +36,10 @@
 	hence "M + {#a#} : ??W"; ..;
 	thus "N : ??W"; by (simp only: N);
       next;
-	fix K; assume "ALL b. elem K b --> (b, a) : r" (is "??A a K")
+	fix K; assume "ALL b. elem K b --> (b, a) : r" (is "??A K")
 	  and N: "N = M0 + K";
 
-	have "??A a K --> M0 + K : ??W" (is "??P K");
+	have "??A K --> M0 + K : ??W" (is "??P K");
 	proof (rule multiset_induct [of _ K]);
 	  from M0; have "M0 + {#} : ??W"; by simp;
 	  thus "??P {#}"; ..;
@@ -47,7 +47,7 @@
 	  fix K x; assume hyp: "??P K";
 	  show "??P (K + {#x#})";
 	  proof;
-	    assume a: "??A a (K + {#x#})";
+	    assume a: "??A (K + {#x#})";
 	    hence "(x, a) : r"; by simp;
 	    with wf_hyp [RS spec]; have b: "ALL M:??W. M + {#x#} : ??W"; ..;
 

--- 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;