1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Apr 19 10:16:51 2012 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Apr 19 11:00:12 2012 +0200
     1.3 @@ -189,10 +189,10 @@
     1.4  \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
     1.5  file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
     1.6  \texttt{components} file does not exist yet and you extracted SPASS to
     1.7 -\texttt{/usr/local/spass-3.7}, create it with the single line
     1.8 +\texttt{/usr/local/spass-3.8ds}, create it with the single line
     1.9  
    1.10  \prew
    1.11 -\texttt{/usr/local/spass-3.7}
    1.12 +\texttt{/usr/local/spass-3.8ds}
    1.13  \postw
    1.14  
    1.15  in it.
    1.16 @@ -203,14 +203,14 @@
    1.17  \texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
    1.18  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
    1.19  \texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.
    1.20 -Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2 and 2.3,
    1.21 -SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
    1.22 +Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2 and~2.3,
    1.23 +SPASS 3.5, 3.7, and 3.8ds, and Vampire 0.6, 1.0, and 1.8%
    1.24  \footnote{Following the rewrite of Vampire, the counter for version numbers was
    1.25  reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
    1.26  than 9.0 or 11.5.}%
    1.27  . Since the ATPs' output formats are neither documented nor stable, other
    1.28 -versions of the ATPs might not work well with Sledgehammer. Ideally,
    1.29 -also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
    1.30 +versions might not work well with Sledgehammer. Ideally,
    1.31 +you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
    1.32  \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
    1.33  \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4'').
    1.34  
    1.35 @@ -825,7 +825,7 @@
    1.36  prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
    1.37  To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
    1.38  that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the
    1.39 -version number (e.g., ``3.7''), or install the prebuilt SPASS package from
    1.40 +version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
    1.41  \download. Sledgehammer requires version 3.5 or above.
    1.42  
    1.43  \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution