| changeset 9747 | 043098ba5098 |
| parent 8442 | 96023903c2df |
| child 9870 | 2374ba026fc6 |
--- a/src/HOL/ex/Puzzle.ML Wed Aug 30 16:24:29 2000 +0200 +++ b/src/HOL/ex/Puzzle.ML Wed Aug 30 16:29:21 2000 +0200 @@ -11,7 +11,7 @@ AddSIs [Puzzle.f_ax]; Goal "! n. k=f(n) --> n <= f(n)"; -by (res_inst_tac [("n","k")] less_induct 1); +by (induct_thm_tac less_induct "k" 1); by (rtac allI 1); by (rename_tac "i" 1); by (case_tac "i" 1);