src/Tools/intuitionistic.ML
changeset 82820 ae85cd17ffbe
parent 82812 ea8d633fd4a8
equal deleted inserted replaced
82803:982e7128ce0f 82820:ae85cd17ffbe
    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));