--- a/src/Doc/Sledgehammer/document/root.tex Mon Jul 29 16:13:35 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Jul 29 17:27:56 2013 +0200
@@ -203,13 +203,14 @@
\url{http://www.vprover.org/}), set the environment variable
\texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
\texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
-\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
+\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL},
+\texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable;
for Alt-Ergo, set the
environment variable \texttt{WHY3\_HOME} to the directory that contains the
\texttt{why3} executable.
-Sledgehammer has been tested with agsyHOL 1.0, Alt-Ergo 0.95.1, E 1.0 to 1.4,
-LEO-II 1.3.4, Satallax 2.2, 2.3, and 2.4, SPASS 3.8ds, and Vampire 0.6 to 2.6.%
+Sledgehammer has been tested with agsyHOL 1.0, Alt-Ergo 0.95.1, E 1.0 to 1.8,
+LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 2.6.%
\footnote{Following the rewrite of Vampire, the counter for version numbers was
reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, and 2.6 are more
recent than 9.0 or 11.5.}%
@@ -217,7 +218,7 @@
versions might not work well with Sledgehammer. Ideally,
you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4'').
+\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.8'').
Similarly, if you want to build CVC3, or found a
Yices or Z3 executable somewhere (e.g.,
@@ -867,9 +868,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 and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or
+executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
install the prebuilt E package from \download. Sledgehammer has been tested with
-versions 1.0 to 1.6.
+versions 1.0 to 1.8.
\item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed
by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use
@@ -900,7 +901,7 @@
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
-\texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.
+\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
\item[\labelitemi] \textbf{\textit{metis}:} Although it is less powerful than
the external provers, Metis itself can be used for proof search.