equal
deleted
inserted
replaced
53 |
53 |
54 (*Attack subgoals using safe inferences*) |
54 (*Attack subgoals using safe inferences*) |
55 fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, |
55 fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, |
56 int_uniq_mp_tac ctxt, |
56 int_uniq_mp_tac ctxt, |
57 biresolve_tac ctxt safe0_brls, |
57 biresolve_tac ctxt safe0_brls, |
58 hyp_subst_tac, |
58 hyp_subst_tac ctxt, |
59 biresolve_tac ctxt safep_brls] ; |
59 biresolve_tac ctxt safep_brls] ; |
60 |
60 |
61 (*Repeatedly attack subgoals using safe inferences*) |
61 (*Repeatedly attack subgoals using safe inferences*) |
62 fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt)); |
62 fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt)); |
63 |
63 |