equal
deleted
inserted
replaced
697 (has_fewer_prems 1, sizef) |
697 (has_fewer_prems 1, sizef) |
698 (prolog_step_tac (make_horns cls) 1)); |
698 (prolog_step_tac (make_horns cls) 1)); |
699 |
699 |
700 (*First, breaks the goal into independent units*) |
700 (*First, breaks the goal into independent units*) |
701 fun safe_best_meson_tac ctxt = |
701 fun safe_best_meson_tac ctxt = |
702 SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN |
702 SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt)); |
703 TRYALL (best_meson_tac size_of_subgoals ctxt)); |
|
704 |
703 |
705 (** Depth-first search version **) |
704 (** Depth-first search version **) |
706 |
705 |
707 val depth_meson_tac = |
706 val depth_meson_tac = |
708 MESON all_tac make_clauses |
707 MESON all_tac make_clauses |
740 THEN_ITER_DEEPEN iter_deepen_limit |
739 THEN_ITER_DEEPEN iter_deepen_limit |
741 (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) |
740 (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) |
742 end)); |
741 end)); |
743 |
742 |
744 fun meson_tac ctxt ths = |
743 fun meson_tac ctxt ths = |
745 SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); |
744 SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); |
746 |
745 |
747 |
746 |
748 (**** Code to support ordinary resolution, rather than Model Elimination ****) |
747 (**** Code to support ordinary resolution, rather than Model Elimination ****) |
749 |
748 |
750 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), |
749 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), |