equal
deleted
inserted
replaced
99 rel_indtac induct THEN_ALL_NEW |
99 rel_indtac induct THEN_ALL_NEW |
100 simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
100 simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
101 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
101 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
102 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
102 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
103 asm_full_simp_tac (HOL_ss addsimps |
103 asm_full_simp_tac (HOL_ss addsimps |
104 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW |
104 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW |
105 (split_conj_tac THEN_ALL_NEW TRY o resolve_tac |
105 (split_conj_tac THEN_ALL_NEW TRY o resolve_tac |
106 @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) |
106 @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) |
107 THEN_ALL_NEW |
107 THEN_ALL_NEW |
108 asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps)) |
108 asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps)) |
109 *} |
109 *} |