1680 |
1680 |
1681 Method \hyperlink{method.slow}{\mbox{\isa{slow}}} is like \hyperlink{method.fast}{\mbox{\isa{fast}}}, but conducts a broader |
1681 Method \hyperlink{method.slow}{\mbox{\isa{slow}}} is like \hyperlink{method.fast}{\mbox{\isa{fast}}}, but conducts a broader |
1682 search: it may, when backtracking from a failed proof attempt, undo |
1682 search: it may, when backtracking from a failed proof attempt, undo |
1683 even the step of proving a subgoal by assumption. |
1683 even the step of proving a subgoal by assumption. |
1684 |
1684 |
1685 \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} are |
1685 \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} |
1686 like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively, |
1686 are like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, |
1687 but use the Simplifier as additional wrapper. The name \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, |
1687 respectively, but use the Simplifier as additional wrapper. The name |
1688 as opposed to \isa{fastsimp}, reflects the behaviour of this popular |
1688 \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, reflects the behaviour of this popular method |
1689 method better without requiring an understanding of its implementation. |
1689 better without requiring an understanding of its implementation. |
1690 |
1690 |
1691 \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain |
1691 \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain |
1692 depth. The start depth is 4 (unless specified explicitly), and the |
1692 depth. The start depth is 4 (unless specified explicitly), and the |
1693 depth is increased iteratively up to 10. Unsafe rules are modified |
1693 depth is increased iteratively up to 10. Unsafe rules are modified |
1694 to preserve the formula they act on, so that it be used repeatedly. |
1694 to preserve the formula they act on, so that it be used repeatedly. |