src/HOL/Tools/ATP/atp_systems.ML
changeset 44967 6e943b3d2767
parent 44963 bf489e54d7f8
child 44970 5e14f591515e
equal deleted inserted replaced
44966:3ea5fae095dc 44967:6e943b3d2767
   415   remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   415   remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   416                (K (200, "mangled_guards?") (* FUDGE *))
   416                (K (200, "mangled_guards?") (* FUDGE *))
   417 val remote_z3_atp =
   417 val remote_z3_atp =
   418   remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
   418   remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
   419 val remote_leo2 =
   419 val remote_leo2 =
   420   remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
   420   remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF, FOF]
   421              (K (100, "simple_higher") (* FUDGE *))
   421              (K (100, "simple_higher") (* FUDGE *))
   422 val remote_satallax =
   422 val remote_satallax =
   423   remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
   423   remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
   424              (K (64, "simple_higher") (* FUDGE *))
   424              (K (64, "simple_higher") (* FUDGE *))
   425 val remote_e_sine =
   425 val remote_e_sine =