# HG changeset patch
# User blanchet
# Date 1332265365 -3600
# Node ID 6f8dfe6c1aea4987c1f346ae6de6ba7108d6d848
# Parent  16e2633f3b4bca059c7b6007504fed1a2e956008
doc update

diff -r 16e2633f3b4b -r 6f8dfe6c1aea doc-src/Sledgehammer/sledgehammer.tex
--- 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