--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 20 15:12:38 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 20 15:26:19 2013 +0100
@@ -207,7 +207,7 @@
val alt_ergo_config : atp_config =
{exec = (["WHY3_HOME"], ["why3"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "--format tff1 --prover alt-ergo --timelimit " ^
+ "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims = [],
known_failures =