# HG changeset patch
# User blanchet
# Date 1283290973 -7200
# Node ID ca7ac998bb36ed09063b74e45d59df40ba2d0717
# Parent  5261cf6b57ca1aab1147f1c4f3d5185b2520282e
update docs

diff -r 5261cf6b57ca -r ca7ac998bb36 doc-src/Sledgehammer/sledgehammer.tex
--- 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