--- a/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 16:57:19 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 17:00:14 2014 +0200
@@ -199,7 +199,7 @@
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.8,
+Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, 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 3.0.%
\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, 2.6, and 3.0 are more
@@ -823,8 +823,8 @@
ATP developed by Bobot et al.\ \cite{alt-ergo}.
It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
\cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME}
-to the directory that contains the \texttt{why3} executable. Sledgehammer has
-been tested with Alt-Ergo 0.95.2 and Why3 0.83.
+to the directory that contains the \texttt{why3} executable. Sledgehammer
+requires Alt-Ergo 0.95.2 and Why3 0.83.
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,