equal
deleted
inserted
replaced
607 THEN_ALL_NEW |
607 THEN_ALL_NEW |
608 REPEAT o etac @{thm exi_neg} |
608 REPEAT o etac @{thm exi_neg} |
609 THEN_ALL_NEW |
609 THEN_ALL_NEW |
610 split_conjs THEN_ALL_NEW |
610 split_conjs THEN_ALL_NEW |
611 asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW |
611 asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW |
612 (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [ |
612 TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW |
613 (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})), |
613 (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) |
614 (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) |
|
615 ]) |
|
616 *} |
614 *} |
617 |
615 |
618 ML {* |
616 ML {* |
619 fun imp_elim_tac case_rules = |
617 fun imp_elim_tac case_rules = |
620 Subgoal.FOCUS (fn {concl, context, ...} => |
618 Subgoal.FOCUS (fn {concl, context, ...} => |