equal
deleted
inserted
replaced
778 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); |
778 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); |
779 |
779 |
780 (*version of bimatch_from_nets_tac that only applies rules that |
780 (*version of bimatch_from_nets_tac that only applies rules that |
781 create precisely n subgoals.*) |
781 create precisely n subgoals.*) |
782 fun n_bimatch_from_nets_tac n = |
782 fun n_bimatch_from_nets_tac n = |
783 biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true; |
783 biresolution_from_nets_tac (Tactic.orderlist o filter (nsubgoalsP n)) true; |
784 |
784 |
785 fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; |
785 fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; |
786 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; |
786 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; |
787 |
787 |
788 (*Two-way branching is allowed only if one of the branches immediately closes*) |
788 (*Two-way branching is allowed only if one of the branches immediately closes*) |