Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Isar_examples/Puzzle.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10007 64bf7da1994a 
--- a/src/HOL/Isar_examples/Puzzle.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -118,7 +118,7 @@
     proof;
       assume "n < f n";
       hence "Suc n <= f n"; by (rule Suc_leI);
-      hence "f (Suc n) <= f (f n)"; by (rule mono [rulified]);
+      hence "f (Suc n) <= f (f n)"; by (rule mono [rule_format]);
       also; have "... < f (Suc n)"; by (rule f_ax);
       finally; have "... < ..."; .; thus False; ..;
     qed;
isabelle