58 (true,all_dupE), (true,not_impE), (true,imp_impE), (true,iff_impE), |
58 (true,all_dupE), (true,not_impE), (true,imp_impE), (true,iff_impE), |
59 (true,all_impE), (true,ex_impE), (true,impE) ]; |
59 (true,all_impE), (true,ex_impE), (true,impE) ]; |
60 |
60 |
61 (*0 subgoals vs 1 or more: the p in safep is for positive*) |
61 (*0 subgoals vs 1 or more: the p in safep is for positive*) |
62 val (safe0_brls, safep_brls) = |
62 val (safe0_brls, safep_brls) = |
63 List.partition (apl(0,op=) o subgoals_of_brl) safe_brls; |
63 List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; |
64 |
64 |
65 (*Attack subgoals using safe inferences -- matching, not resolution*) |
65 (*Attack subgoals using safe inferences -- matching, not resolution*) |
66 val safe_step_tac = FIRST' [eq_assume_tac, |
66 val safe_step_tac = FIRST' [eq_assume_tac, |
67 eq_mp_tac, |
67 eq_mp_tac, |
68 bimatch_tac safe0_brls, |
68 bimatch_tac safe0_brls, |