| changeset 9736 | 332fab43628f |
| parent 8683 | 9d3e8c4a0287 |
| child 9747 | 043098ba5098 |
--- a/src/HOL/ex/Recdefs.ML Tue Aug 29 22:31:36 2000 +0200 +++ b/src/HOL/ex/Recdefs.ML Wed Aug 30 10:21:19 2000 +0200 @@ -12,12 +12,12 @@ Addsimps g.simps; Goal "g x < Suc x"; -by (res_inst_tac [("u","x")] g.induct 1); +by (res_inst_tac [("x","x")] g.induct 1); by Auto_tac; qed "g_terminates"; Goal "g x = 0"; -by (res_inst_tac [("u","x")] g.induct 1); +by (res_inst_tac [("x","x")] g.induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates]))); qed "g_zero";