src/HOL/Isar_examples/Puzzle.thy
changeset 9906 5c027cca6262
parent 9870 2374ba026fc6
child 9941 fe05af7ec816
     1.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Thu Sep 07 21:06:55 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Thu Sep 07 21:10:11 2000 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4      proof;
     1.5        assume "n < f n";
     1.6        hence "Suc n <= f n"; by (rule Suc_leI);
     1.7 -      hence "f (Suc n) <= f (f n)"; by (rule mono [rulify]);
     1.8 +      hence "f (Suc n) <= f (f n)"; by (rule mono [rulified]);
     1.9        also; have "... < f (Suc n)"; by (rule f_ax);
    1.10        finally; have "... < ..."; .; thus False; ..;
    1.11      qed;