# HG changeset patch
# User blanchet
# Date 1375111676 -7200
# Node ID ea7cf7b14fdde0b484b5dbdcae0768bb0d2f9abf
# Parent  1ac8a0d0ddb1190782daa361a87349eb9e9f9f58
updated Sledgehammer prover versions

diff -r 1ac8a0d0ddb1 -r ea7cf7b14fdd src/Doc/Sledgehammer/document/root.tex
--- 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.