equal
deleted
inserted
replaced
84 THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN' |
84 THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN' |
85 asm_full_simp_tac |
85 asm_full_simp_tac |
86 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) |
86 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) |
87 *} |
87 *} |
88 |
88 |
89 ML {* |
89 |
90 fun all_eqvts ctxt = |
90 ML {* |
91 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
91 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt) |
92 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
92 fun all_eqvts ctxt = |
|
93 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
|
94 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
93 *} |
95 *} |
94 |
96 |
95 ML {* |
97 ML {* |
96 fun constr_rsp_tac inj rsp equivps = |
98 fun constr_rsp_tac inj rsp equivps = |
97 let |
99 let |