# HG changeset patch
# User blanchet
# Date 1283286637 -7200
# Node ID 5261cf6b57ca1aab1147f1c4f3d5185b2520282e
# Parent  820b8221ed48f9392eef756e6a6030317b5a37c2
update docs

diff -r 820b8221ed48 -r 5261cf6b57ca doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 31 22:27:33 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 31 22:30:37 2010 +0200
@@ -349,19 +349,13 @@
 \end{enum}
 
 Default values are indicated in square brackets. Boolean options have a negated
-counterpart (e.g., \textit{debug} vs.\ \textit{no\_debug}). When setting
+counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
 Boolean options, ``= \textit{true}'' may be omitted.
 
 \subsection{Mode of Operation}
 \label{mode-of-operation}
 
 \begin{enum}
-%\optrue{blocking}{non\_blocking}
-%Specifies whether the \textbf{sledgehammer} command should operate synchronously.
-%The asynchronous (non-blocking) mode lets the user start proving the putative
-%theorem while Sledgehammer looks for a counterexample, but it can also be more
-%confusing. For technical reasons, automatic runs currently always block.
-
 \opnodefault{atps}{string}
 Specifies the ATPs (automated theorem provers) to use as a space-separated list
 (e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported:
@@ -414,6 +408,12 @@
 \opnodefault{atp}{string}
 Alias for \textit{atps}.
 
+\opfalse{blocking}{non\_blocking}
+Specifies whether the \textbf{sledgehammer} command should operate
+synchronously. The asynchronous (non-blocking) mode lets the user start proving
+the putative theorem manually while Sledgehammer looks for a proof, but it can
+also be more confusing.
+
 \opfalse{overlord}{no\_overlord}
 Specifies whether Sledgehammer should put its temporary files in
 \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for