--- a/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 17:00:14 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 17:16:02 2014 +0200
@@ -208,7 +208,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.8'').
+\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
Similarly, if you want to build CVC3, or found a
Yices or Z3 executable somewhere (e.g.,
@@ -897,7 +897,7 @@
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
-``2.6''). Sledgehammer has been tested with versions 0.6 to 3.0.
+``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0.
Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at