| changeset 5983 | 79e301a6a51b |
| parent 5599 | 95a92bc7a591 |
| child 8423 | 3c19160b6432 |
--- a/src/HOL/ex/Primrec.ML Fri Nov 27 16:54:59 1998 +0100 +++ b/src/HOL/ex/Primrec.ML Fri Nov 27 17:00:30 1998 +0100 @@ -50,7 +50,6 @@ Goal "j < ack(i,j)"; by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); by (ALLGOALS Asm_simp_tac); -by (ALLGOALS trans_tac); qed "less_ack2"; AddIffs [less_ack2];