src/FOLP/intprover.ML
changeset 15570 8d8c70b41bab
parent 9263 53e09e592278
child 17496 26535df536ae
equal deleted inserted replaced
15569:1b3115d1a8df 15570:8d8c70b41bab
    48       (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
    48       (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
    49       (true,all_impE), (true,ex_impE), (true,impE) ];
    49       (true,all_impE), (true,ex_impE), (true,impE) ];
    50 
    50 
    51 (*0 subgoals vs 1 or more: the p in safep is for positive*)
    51 (*0 subgoals vs 1 or more: the p in safep is for positive*)
    52 val (safe0_brls, safep_brls) =
    52 val (safe0_brls, safep_brls) =
    53     partition (apl(0,op=) o subgoals_of_brl) safe_brls;
    53     List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
    54 
    54 
    55 (*Attack subgoals using safe inferences*)
    55 (*Attack subgoals using safe inferences*)
    56 val safe_step_tac = FIRST' [uniq_assume_tac,
    56 val safe_step_tac = FIRST' [uniq_assume_tac,
    57                             int_uniq_mp_tac,
    57                             int_uniq_mp_tac,
    58                             biresolve_tac safe0_brls,
    58                             biresolve_tac safe0_brls,