equal
deleted
inserted
replaced
52 val (safe0_brls, safep_brls) = |
52 val (safe0_brls, safep_brls) = |
53 partition (apl(0,op=) o subgoals_of_brl) safe_brls; |
53 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 IFOLP_Lemmas.uniq_mp_tac, |
57 int_uniq_mp_tac, |
58 biresolve_tac safe0_brls, |
58 biresolve_tac safe0_brls, |
59 hyp_subst_tac, |
59 hyp_subst_tac, |
60 biresolve_tac safep_brls] ; |
60 biresolve_tac safep_brls] ; |
61 |
61 |
62 (*Repeatedly attack subgoals using safe inferences*) |
62 (*Repeatedly attack subgoals using safe inferences*) |