Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Fri, 30 Apr 1999 18:25:10 +0200
changeset 6559 fa203026941c
parent 6558 120ff48e8618
child 6560 1436349f8b28
tuned;
src/HOL/Isar_examples/NatSum.thy file | annotate | diff | comparison | revisions
src/HOL/Isar_examples/ROOT.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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";
-
isabelle