# HG changeset patch
# User blanchet
# Date 1396524598 -7200
# Node ID a0c4a162bd130e0e007fdee27ecd5b058b90156d
# Parent  5a93b8f928a29f7fe46530b5332e607daeff1148
updated Why3 version in docs

diff -r 5a93b8f928a2 -r a0c4a162bd13 src/Doc/Sledgehammer/document/root.tex
--- 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,