# HG changeset patch
# User blanchet
# Date 1284193248 -7200
# Node ID 6ec8d46836996a1df286bed73cab224aafa79083
# Parent  b6c4385ab400682c1f3b31d7b65d9c69ac6662c3
document changes to Auto Nitpick

diff -r b6c4385ab400 -r 6ec8d4683699 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Sat Sep 11 10:20:25 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Sat Sep 11 10:20:48 2010 +0200
@@ -121,11 +121,10 @@
 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
 
 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
-Nitpick also provides an automatic mode that can be enabled using the
-``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
-mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
-The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
-the ``Auto Counterexample Time Limit'' option.
+Nitpick also provides an automatic mode that can be enabled via the ``Auto
+Nitpick'' option from the ``Isabelle'' menu in Proof General. In this mode,
+Nitpick is run on every newly entered theorem. The time limit for Auto Nitpick
+and other automatic tools can be set using the ``Auto Tools Time Limit'' option.
 
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
@@ -1883,14 +1882,15 @@
 
 You can instruct Nitpick to run automatically on newly entered theorems by
 enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
-General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
-and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
-\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
-(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
-disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
-\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
-Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
-concise.
+General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}),
+\textit{assms} (\S\ref{mode-of-operation}), and \textit{mono}
+(\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking}
+(\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and
+\textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_threads}
+(\S\ref{optimizations}) is taken to be 1, \textit{max\_potential}
+(\S\ref{output-format}) is taken to be 0, and \textit{timeout}
+(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in
+Proof General's ``Isabelle'' menu. Nitpick's output is also more concise.
 
 The number of options can be overwhelming at first glance. Do not let that worry
 you: Nitpick's defaults have been chosen so that it almost always does the right
@@ -2171,7 +2171,8 @@
 scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
 performs a monotonicity check on the type. Setting this option to \textit{true}
 can reduce the number of scopes tried, but it can also diminish the chance of
-finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
+finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}. The
+option is implicitly set to \textit{true} for automatic runs.
 
 \nopagebreak
 {\small See also \textit{card} (\S\ref{scope-of-search}),
@@ -2527,7 +2528,7 @@
 \opdefault{max\_threads}{int}{0}
 Specifies the maximum number of threads to use in Kodkod. If this option is set
 to 0, Kodkod will compute an appropriate value based on the number of processor
-cores available.
+cores available. The option is implicitly set to 1 for automatic runs.
 
 \nopagebreak
 {\small See also \textit{batch\_size} (\S\ref{optimizations}) and