doc-src/Nitpick/nitpick.tex
changeset 48588 a0125644ccff
parent 47113 99a2a541c125
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Apr 24 09:47:40 2012 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Apr 24 09:47:40 2012 +0200
     1.3 @@ -2534,14 +2534,15 @@
     1.4  {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
     1.5  
     1.6  \opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5}
     1.7 -Specifies the maximum number of seconds that the \textit{auto} tactic should use
     1.8 -when checking a counterexample, and similarly that \textit{lexicographic\_order}
     1.9 -and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
    1.10 -predicate is well-founded. Nitpick tries to honor this constraint as well as it
    1.11 -can but offers no guarantees.
    1.12 +Specifies the maximum number of seconds that should be used by internal
    1.13 +tactics---\textit{lexicographic\_order} and \textit{size\_change} when checking
    1.14 +whether a (co)in\-duc\-tive predicate is well-founded, \textit{auto} tactic when
    1.15 +checking a counterexample, or the monotonicity inference. Nitpick tries to honor
    1.16 +this constraint but offers no guarantees.
    1.17  
    1.18  \nopagebreak
    1.19  {\small See also \textit{wf} (\S\ref{scope-of-search}),
    1.20 +\textit{mono} (\S\ref{scope-of-search}),
    1.21  \textit{check\_potential} (\S\ref{authentication}),
    1.22  and \textit{check\_genuine} (\S\ref{authentication}).}
    1.23  \end{enum}