| changeset 9747 | 043098ba5098 |
| parent 7958 | f531589c9fc1 |
| child 13630 | a013a9dd370f |
--- a/src/HOL/MiniML/MiniML.ML Wed Aug 30 16:24:29 2000 +0200 +++ b/src/HOL/MiniML/MiniML.ML Wed Aug 30 16:29:21 2000 +0200 @@ -114,7 +114,7 @@ qed "free_tv_alpha"; Goal "!!(k::nat). n <= n + k"; -by (res_inst_tac [("n","k")] nat_induct 1); +by (induct_thm_tac nat_induct "k" 1); by (Simp_tac 1); by (Asm_simp_tac 1); val aux_plus = result();