# HG changeset patch # User blanchet # Date 1572013616 -7200 # Node ID 718255bde391ffb493f72a008073d7b0ee085d0a # Parent d4ef7617e31e746fd8ca70dbb485fa76d29a74c7 invoke remote Vampire with higher-order (THF) syntax diff -r d4ef7617e31e -r 718255bde391 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 16:18:22 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 16:26:56 2019 +0200 @@ -620,9 +620,9 @@ | res => res fun get_remote_system name versions = - Synchronized.change_result remote_systems - (fn systems => (if null systems then get_remote_systems () else systems) - |> `(`(find_remote_system name versions))) + Synchronized.change_result remote_systems (fn systems => + (if null systems then get_remote_systems () else systems) + |> `(`(find_remote_system name versions))) fun the_remote_system name versions = (case get_remote_system name versions of @@ -694,8 +694,8 @@ [("refutation.", "end_refutation.")] [] Hypothesis (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *)) val remote_vampire = - remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"] - (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_command) (* FUDGE *)) + remotify_atp vampire "Vampire" ["THF-4.4"] + (K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = remotify_atp zipperposition "Zipperpin" ["1.5"]