# HG changeset patch
# User blanchet
# Date 1396537214 -7200
# Node ID d8ecce5d51cdcd3706ececdf4fc19abf6167f883
# Parent  8fb4515818f7d106b729f6a6c8a512a719abe8df
use Alt-Ergo 0.95.2, the latest and greatest version

diff -r 8fb4515818f7 -r d8ecce5d51cd src/Doc/Sledgehammer/document/root.tex
--- 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,
diff -r 8fb4515818f7 -r d8ecce5d51cd src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 03 16:57:19 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 03 17:00:14 2014 +0200
@@ -237,7 +237,7 @@
 val alt_ergo_config : atp_config =
   {exec = K (["WHY3_HOME"], ["why3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
-       "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
+       "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^
        string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims = [],
    known_failures =