equal
deleted
inserted
replaced
60 |
60 |
61 ML {* |
61 ML {* |
62 fun fvbv_rsp_tac induct fvbv_simps ctxt = |
62 fun fvbv_rsp_tac induct fvbv_simps ctxt = |
63 rtac induct THEN_ALL_NEW |
63 rtac induct THEN_ALL_NEW |
64 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW |
64 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW |
65 asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps alphas} @ fvbv_simps)) THEN_ALL_NEW |
65 asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps set.simps append.simps alphas} @ fvbv_simps)) THEN_ALL_NEW |
66 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
66 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
67 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
67 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
68 TRY o blast_tac (claset_of ctxt) |
68 TRY o blast_tac (claset_of ctxt) |
69 *} |
69 *} |
70 |
70 |