doc update
authorblanchet
Tue, 20 Mar 2012 18:42:45 +0100
changeset 479266f8dfe6c1aea
parent 47925 16e2633f3b4b
child 47930 8e1b14bf0190
doc update
doc-src/Sledgehammer/sledgehammer.tex
     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