equal
deleted
inserted
replaced
500 fun check_tac st = |
500 fun check_tac st = |
501 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) |
501 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) |
502 then Seq.empty else Seq.single st; |
502 then Seq.empty else Seq.single st; |
503 |
503 |
504 |
504 |
505 (* net_resolve_tac actually made it slower... *) |
505 (* resolve_from_net_tac actually made it slower... *) |
506 fun prolog_step_tac ctxt horns i = |
506 fun prolog_step_tac ctxt horns i = |
507 (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN |
507 (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN |
508 TRYALL_eq_assume_tac; |
508 TRYALL_eq_assume_tac; |
509 |
509 |
510 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) |
510 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) |
742 (*This version does only one inference per call; |
742 (*This version does only one inference per call; |
743 having only one eq_assume_tac speeds it up!*) |
743 having only one eq_assume_tac speeds it up!*) |
744 fun prolog_step_tac' ctxt horns = |
744 fun prolog_step_tac' ctxt horns = |
745 let val (horn0s, _) = (*0 subgoals vs 1 or more*) |
745 let val (horn0s, _) = (*0 subgoals vs 1 or more*) |
746 take_prefix Thm.no_prems horns |
746 take_prefix Thm.no_prems horns |
747 val nrtac = net_resolve_tac horns |
747 val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns) |
748 in fn i => eq_assume_tac i ORELSE |
748 in fn i => eq_assume_tac i ORELSE |
749 match_tac ctxt horn0s i ORELSE (*no backtracking if unit MATCHES*) |
749 match_tac ctxt horn0s i ORELSE (*no backtracking if unit MATCHES*) |
750 ((assume_tac ctxt i APPEND nrtac i) THEN check_tac) |
750 ((assume_tac ctxt i APPEND nrtac i) THEN check_tac) |
751 end; |
751 end; |
752 |
752 |