changeset 5462 | 7c5b2a8adbf0 |
parent 5148 | 74919e8f221c |
child 5599 | 95a92bc7a591 |
--- a/src/HOL/ex/Primrec.ML Thu Sep 10 17:30:50 1998 +0200 +++ b/src/HOL/ex/Primrec.ML Thu Sep 10 17:32:07 1998 +0200 @@ -201,6 +201,7 @@ by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1); by Safe_tac; by (Asm_simp_tac 1); +by (rtac exI 1); by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1); qed "COMP_map_lemma";