equal
deleted
inserted
replaced
23 (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i) |
23 (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i) |
24 end); |
24 end); |
25 |
25 |
26 fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt; |
26 fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt; |
27 |
27 |
28 fun bires_tac ctxt = Tactic.biresolution_from_nets_tac ctxt Context_Rules.orderlist; |
28 fun bires_tac ctxt = Bires.biresolution_from_nets_tac ctxt Bires.tag_ord NONE; |
29 |
29 |
30 fun safe_step_tac ctxt = |
30 fun safe_step_tac ctxt = |
31 Context_Rules.Swrap ctxt |
31 Context_Rules.Swrap ctxt |
32 (eq_assume_tac ORELSE' |
32 (eq_assume_tac ORELSE' |
33 bires_tac ctxt true (Context_Rules.netpair_bang ctxt)); |
33 bires_tac ctxt true (Context_Rules.netpair_bang ctxt)); |