1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Mar 20 18:42:45 2012 +0100
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Mar 20 18:42:45 2012 +0100
1.3 @@ -791,8 +791,9 @@
1.4 \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
1.5 developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
1.6 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
1.7 -executable, or install the prebuilt E package from \download. Sledgehammer has
1.8 -been tested with versions 1.0 to 1.4.
1.9 +executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or
1.10 +install the prebuilt E package from \download. Sledgehammer has been tested with
1.11 +versions 1.0 to 1.4.
1.12
1.13 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
1.14 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
1.15 @@ -815,8 +816,9 @@
1.16 \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
1.17 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
1.18 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
1.19 -that contains the \texttt{SPASS} executable, or install the prebuilt SPASS
1.20 -package from \download. Sledgehammer requires version 3.5 or above.
1.21 +that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the
1.22 +version number (e.g., ``3.7''), or install the prebuilt SPASS package from
1.23 +\download. Sledgehammer requires version 3.5 or above.
1.24
1.25 \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
1.26 prover developed by Andrei Voronkov and his colleagues