# HG changeset patch
# User wenzelm
# Date 930603919 -7200
# Node ID 60a5ee0ca81db43bb83cc47d36325bf58bddff13
# Parent  80f88b762816584e2a8fb108909857485e6579df
updated;

diff -r 80f88b762816 -r 60a5ee0ca81d src/HOL/Isar_examples/NatSum.thy
--- 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;
 
 
diff -r 80f88b762816 -r 60a5ee0ca81d src/HOL/Isar_examples/Peirce.thy
--- 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;