equal
deleted
inserted
replaced
218 |
218 |
219 |
219 |
220 ML {* |
220 ML {* |
221 fun alpha_inj_tac dist_inj intrs elims = |
221 fun alpha_inj_tac dist_inj intrs elims = |
222 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' |
222 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' |
223 rtac @{thm iffI} THEN' RANGE [ |
223 (rtac @{thm iffI} THEN' RANGE [ |
224 (eresolve_tac elims THEN_ALL_NEW |
224 (eresolve_tac elims THEN_ALL_NEW |
225 asm_full_simp_tac (HOL_ss addsimps dist_inj) |
225 asm_full_simp_tac (HOL_ss addsimps dist_inj) |
226 ), |
226 ), |
227 (asm_full_simp_tac (HOL_ss addsimps intrs))] |
227 asm_full_simp_tac (HOL_ss addsimps intrs)]) |
228 *} |
228 *} |
229 |
229 |
230 ML {* |
230 ML {* |
231 fun build_alpha_inj_gl thm = |
231 fun build_alpha_inj_gl thm = |
232 let |
232 let |