--- a/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Apr 03 13:29:58 2014 +0200
@@ -824,8 +824,7 @@
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.1 and an unidentified development version of
-Why3.
+been tested with 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,