# HG changeset patch # User blanchet # Date 1367569644 -7200 # Node ID 3f2eacb8235a85b1c1d50f0762010f29f1a104df # Parent af2e0b2c4d7efea20eaaf86f3b4c69595700d072 tuning diff -r af2e0b2c4d7e -r 3f2eacb8235a src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri May 03 10:26:34 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri May 03 10:27:24 2013 +0200 @@ -226,8 +226,8 @@ (* E *) -fun is_e_at_least_1_3 () = (string_ord (getenv "E_VERSION", "1.3") <> LESS) -fun is_e_at_least_1_6 () = (string_ord (getenv "E_VERSION", "1.6") <> LESS) +fun is_e_at_least_1_3 () = string_ord (getenv "E_VERSION", "1.3") <> LESS +fun is_e_at_least_1_6 () = string_ord (getenv "E_VERSION", "1.6") <> LESS val tstp_proof_delims = [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"), @@ -530,10 +530,8 @@ (* Vampire 1.8 has TFF support, but the support was buggy until revision 1435 (or shortly before). *) -fun is_vampire_at_least_1_8 () = - string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS -fun is_vampire_beyond_1_8 () = - string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER +fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS +fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)