updated;

--- a/src/HOL/Isar_examples/NatSum.thy	Mon Jun 28 23:02:38 1999 +0200
+++ b/src/HOL/Isar_examples/NatSum.thy	Mon Jun 28 23:05:19 1999 +0200
@@ -35,10 +35,10 @@
 
 theorem "2 * sum (%i. i) (Suc n) = n * Suc n";
 proof same;
-  refine simp_tac;
-  refine (induct n);
-  refine simp_tac;
-  refine asm_simp_tac;
+  apply simp_tac;
+  apply (induct n);
+  apply simp_tac;
+  apply asm_simp_tac;
 qed_with sum_of_naturals;
 
 

--- a/src/HOL/Isar_examples/Peirce.thy	Mon Jun 28 23:02:38 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Mon Jun 28 23:05:19 1999 +0200
@@ -30,11 +30,9 @@
   assume ABA: "(A --> B) --> A";
   show A;
   proof (rule classical);
-
-    assume AB: "A --> B";
+    presume AB: "A --> B";
     from ABA AB; show A; ..;
-
-    next;
+  next;
     assume notA: "~ A";
     show "A --> B";
     proof;