# HG changeset patch
# User blanchet
# Date 1443814149 -7200
# Node ID ea605d019e9f361eb3d00375f0d041a2d1659b02
# Parent  a48388351990bd5b7dd223d31163764219b0bbd5
updated docs

diff -r a48388351990 -r ea605d019e9f src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Fri Oct 02 21:24:37 2015 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Fri Oct 02 21:29:09 2015 +0200
@@ -118,22 +118,22 @@
 must find a model for the axioms. If it finds no model, we have an indication
 that the axioms might be unsatisfiable.
 
-For Isabelle/jEdit users, Nitpick provides an automatic mode that can be enabled
-via the ``Auto Nitpick'' option under ``Plugins > Plugin Options > Isabelle >
-General.'' In this mode, Nitpick is run on every newly entered theorem.
+Nitpick provides an automatic mode that can be enabled via the ``Auto Nitpick''
+option under ``Plugins > Plugin Options > Isabelle > General'' in
+Isabelle/jEdit. In this mode, Nitpick is run on every newly entered theorem.
 
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
 
-\newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
-in.\allowbreak tum.\allowbreak de}}
+\newcommand\authoremail{\texttt{jasmin.blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
+inria\allowbreak .\allowbreak fr}}
 
 To run Nitpick, you must also make sure that the theory \textit{Nitpick} is
 imported---this is rarely a problem in practice since it is part of
 \textit{Main}. The examples presented in this manual can be found
 in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory.
 The known bugs and limitations at the time of writing are listed in
-\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either
+\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning
 the tool or the manual should be directed to the author at \authoremail.
 
 \vskip2.5\smallskipamount
@@ -1740,18 +1740,18 @@
 format (\S\ref{output-format}), regression testing (\S\ref{regression-testing}),
 optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
 
-If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can
-be enabled via the ``Auto Nitpick'' option under ``Plugins > Plugin Options
-> Isabelle > General.'' For automatic runs,
+Nitpick also provides an automatic mode that can be enabled via the
+``Auto Nitpick'' option under ``Plugins > Plugin Options > Isabelle > General''
+in Isabelle/jEdit. 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
+(\S\ref{scope-of-search}) are implicitly enabled,
+\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, \textit{max\_threads}
 (\S\ref{optimizations}) is taken to be 1, and \textit{timeout}
-(\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in jEdit. Nitpick's
-output is also more concise.
+(\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in
+Isabelle/jEdit. 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
@@ -1781,19 +1781,13 @@
 \end{enum}
 
 Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
-have a negated counterpart (e.g., \textit{blocking} vs.\
-\textit{non\_blocking}). When setting them, ``= \textit{true}'' may be omitted.
+have a negated counterpart (e.g., \textit{mono} vs.\
+\textit{non\_mono}). When setting them, ``= \textit{true}'' may be omitted.
 
 \subsection{Mode of Operation}
 \label{mode-of-operation}
 
 \begin{enum}
-\optrue{blocking}{non\_blocking}
-Specifies whether the \textbf{nitpick} command should operate synchronously.
-The asynchronous (non-blocking) mode lets the user start proving the putative
-theorem while Nitpick looks for a counterexample, but it can also be more
-confusing. For technical reasons, automatic runs currently always block.
-
 \optrue{falsify}{satisfy}
 Specifies whether Nitpick should look for falsifying examples (countermodels) or
 satisfying examples (models). This manual assumes throughout that