# 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