--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Mar 20 18:42:45 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Mar 20 18:42:45 2012 +0100
@@ -791,8 +791,9 @@
\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.
+executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or
+install the prebuilt E package from \download. Sledgehammer has 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},
@@ -815,8 +816,9 @@
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
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.
+that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the
+version number (e.g., ``3.7''), or install the prebuilt SPASS 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