1.1 --- a/doc-src/Nitpick/nitpick.tex	Sat Sep 11 10:20:25 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sat Sep 11 10:20:48 2010 +0200
     1.3 @@ -121,11 +121,10 @@
     1.4  in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
     1.5  
     1.6  Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
     1.7 -Nitpick also provides an automatic mode that can be enabled using the
     1.8 -``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
     1.9 -mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
    1.10 -The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
    1.11 -the ``Auto Counterexample Time Limit'' option.
    1.12 +Nitpick also provides an automatic mode that can be enabled via the ``Auto
    1.13 +Nitpick'' option from the ``Isabelle'' menu in Proof General. In this mode,
    1.14 +Nitpick is run on every newly entered theorem. The time limit for Auto Nitpick
    1.15 +and other automatic tools can be set using the ``Auto Tools Time Limit'' option.
    1.16  
    1.17  \newbox\boxA
    1.18  \setbox\boxA=\hbox{\texttt{nospam}}
    1.19 @@ -1883,14 +1882,15 @@
    1.20  
    1.21  You can instruct Nitpick to run automatically on newly entered theorems by
    1.22  enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
    1.23 -General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
    1.24 -and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
    1.25 -\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
    1.26 -(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
    1.27 -disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
    1.28 -\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
    1.29 -Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
    1.30 -concise.
    1.31 +General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}),
    1.32 +\textit{assms} (\S\ref{mode-of-operation}), and \textit{mono}
    1.33 +(\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking}
    1.34 +(\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and
    1.35 +\textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_threads}
    1.36 +(\S\ref{optimizations}) is taken to be 1, \textit{max\_potential}
    1.37 +(\S\ref{output-format}) is taken to be 0, and \textit{timeout}
    1.38 +(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in
    1.39 +Proof General's ``Isabelle'' menu. Nitpick's output is also more concise.
    1.40  
    1.41  The number of options can be overwhelming at first glance. Do not let that worry
    1.42  you: Nitpick's defaults have been chosen so that it almost always does the right
    1.43 @@ -2171,7 +2171,8 @@
    1.44  scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
    1.45  performs a monotonicity check on the type. Setting this option to \textit{true}
    1.46  can reduce the number of scopes tried, but it can also diminish the chance of
    1.47 -finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
    1.48 +finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}. The
    1.49 +option is implicitly set to \textit{true} for automatic runs.
    1.50  
    1.51  \nopagebreak
    1.52  {\small See also \textit{card} (\S\ref{scope-of-search}),
    1.53 @@ -2527,7 +2528,7 @@
    1.54  \opdefault{max\_threads}{int}{0}
    1.55  Specifies the maximum number of threads to use in Kodkod. If this option is set
    1.56  to 0, Kodkod will compute an appropriate value based on the number of processor
    1.57 -cores available.
    1.58 +cores available. The option is implicitly set to 1 for automatic runs.
    1.59  
    1.60  \nopagebreak
    1.61  {\small See also \textit{batch\_size} (\S\ref{optimizations}) and