# HG changeset patch
# User wenzelm
# Date 925489510 -7200
# Node ID fa203026941c8782ec79909aa893aa751bafce45
# Parent  120ff48e8618ac79661c49007840a086e59a9945
tuned;

diff -r 120ff48e8618 -r fa203026941c src/HOL/Isar_examples/NatSum.thy
--- a/src/HOL/Isar_examples/NatSum.thy	Fri Apr 30 18:13:55 1999 +0200
+++ b/src/HOL/Isar_examples/NatSum.thy	Fri Apr 30 18:25:10 1999 +0200
@@ -62,7 +62,7 @@
 theorem sum_of_odds: "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
 proof (induct n);
   show "??P 0"; by simp;
-  fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp add: hyp);
+  fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp);
 qed;
 
 text "The second version tells more about what is going on during the
diff -r 120ff48e8618 -r fa203026941c src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Fri Apr 30 18:13:55 1999 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Fri Apr 30 18:25:10 1999 +0200
@@ -10,4 +10,3 @@
 use_thy "Cantor";
 use_thy "ExprCompiler";
 use_thy "NatSum";
-