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 9870 2374ba026fc6
parent 8902 a705822f4e2a
child 9906 5c027cca6262 
--- a/src/HOL/Isar_examples/Puzzle.thy	Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy	Wed Sep 06 08:04:41 2000 +0200
@@ -26,7 +26,7 @@
   {;
     fix k;
     have "ALL x. k = f x --> ?C x" (is "?Q k");
-    proof (rule less_induct);
+    proof (rule nat_less_induct);
       fix k; assume hyp: "ALL m<k. ?Q m";
       show "?Q k";
       proof;
isabelle