--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 31 22:30:37 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 31 23:42:53 2010 +0200
@@ -333,8 +333,9 @@
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
Sledgehammer's options are categorized as follows:\ mode of operation
-(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), output
-format (\S\ref{output-format}), and timeouts (\S\ref{timeouts}).
+(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
+relevance filter (\S\ref{relevance-filter}), output format
+(\S\ref{output-format}), and authentication (\S\ref{authentication}).
The descriptions below refer to the following syntactic quantities:
@@ -349,7 +350,7 @@
\end{enum}
Default values are indicated in square brackets. Boolean options have a negated
-counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
+counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
Boolean options, ``= \textit{true}'' may be omitted.
\subsection{Mode of Operation}
@@ -408,6 +409,12 @@
\opnodefault{atp}{string}
Alias for \textit{atps}.
+\opdefault{timeout}{time}{$\mathbf{60}$ s}
+Specifies the maximum amount of time that the ATPs should spend searching for a
+proof. For historical reasons, the default value of this option can be
+overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
+menu in Proof General.
+
\opfalse{blocking}{non\_blocking}
Specifies whether the \textbf{sledgehammer} command should operate
synchronously. The asynchronous (non-blocking) mode lets the user start proving
@@ -501,15 +508,25 @@
\end{enum}
-\subsection{Timeouts}
-\label{timeouts}
+\subsection{Authentication}
+\label{authentication}
+
+\begin{enum}
+\opnodefault{expect}{string}
+Specifies the expected outcome, which must be one of the following:
\begin{enum}
-\opdefault{timeout}{time}{$\mathbf{60}$ s}
-Specifies the maximum amount of time that the ATPs should spend looking for a
-proof. For historical reasons, the default value of this option can be
-overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
-menu in Proof General.
+\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially unsound) proof.
+\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.
+\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some problem.
+\end{enum}
+
+Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
+(otherwise) if the actual outcome differs from the expected outcome. This option
+is useful for regression testing.
+
+\nopagebreak
+{\small See also \textit{blocking} (\S\ref{mode-of-operation}).}
\end{enum}
\let\em=\sl