# HG changeset patch
# User blanchet
# Date 1327005432 -3600
# Node ID 14459b9671a16b4f0048f030f3661feb8df3cfbe
# Parent  e9a2d81fa7258941504e0d82d83bb42c1bf258c2
more doc updates

diff -r e9a2d81fa725 -r 14459b9671a1 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Jan 19 21:37:12 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Jan 19 21:37:12 2012 +0100
@@ -751,22 +751,24 @@
 \begin{enum}
 \opnodefaultbrk{provers}{string}
 Specifies the automatic provers to use as a space-separated list (e.g.,
-``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}''). The following local
-provers are supported:
+``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}'').
+Provers can be run locally or remotely; see \S\ref{installation} for
+installation instructions.
+
+The following local provers are supported:
 
 \begin{enum}
 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
 executable, including the file name, or install the prebuilt CVC3 package from
-\download. Sledgehammer has been tested with version 2.2. See
-\S\ref{installation} for details.
+\download. Sledgehammer has been tested with version 2.2.
 
 \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
 developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
 executable, or install the prebuilt E package from \download. Sledgehammer has
-been tested with versions 1.0 to 1.4. See \S\ref{installation} for details.
+been tested with versions 1.0 to 1.4.
 
 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
@@ -790,8 +792,7 @@
 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
 that contains the \texttt{SPASS} executable, or install the prebuilt SPASS
-package from \download. Sledgehammer requires version 3.5 or above. See
-\S\ref{installation} for details.
+package from \download. Sledgehammer requires version 3.5 or above.
 
 \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
 prover developed by Andrei Voronkov and his colleagues
@@ -820,7 +821,7 @@
 executable.
 \end{enum}
 
-In addition, the following remote provers are supported:
+The following remote provers are supported:
 
 \begin{enum}
 \item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
@@ -1121,8 +1122,9 @@
 \opfalse{sound}{unsound}
 Specifies whether Sledgehammer should run in its fully sound mode. In that mode,
 quasi-sound type encodings (which are the default) are made fully sound, at the
-cost of some clutter in the generated problems. This option is ignored if
-\textit{type\_enc} is set to an unsound encoding.
+cost of some clutter in the generated problems.
+This option is ignored if \textit{type\_enc} is deliberately set to an encoding
+that is not sound or quasi-sound.
 \end{enum}
 
 \subsection{Relevance Filter}