# HG changeset patch # User blanchet # Date 1306068632 -7200 # Node ID c124032ac96fd554ca8e007da4c725a44bcb20f9 # Parent cabb3a9478942b2310a6e992020f5bc31a73253f added Waldmeister diff -r cabb3a947894 -r c124032ac96f src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:49:35 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:50:32 2011 +0200 @@ -39,6 +39,7 @@ val tofof_eN : string val sine_eN : string val snarkN : string + val waldmeisterN : string val z3_atpN : string val remote_prefix : string val remote_atp : @@ -100,6 +101,7 @@ val tofof_eN = "tofof_e" val sine_eN = "sine_e" val snarkN = "snark" +val waldmeisterN = "waldmeister" val remote_prefix = "remote_" structure Data = Theory_Data @@ -414,6 +416,10 @@ remote_atp snarkN "SNARK" ["20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Conjecture [TFF, FOF] (K (250, ["simple"]) (* FUDGE *)) +val remote_waldmeister = + remote_atp waldmeisterN "Waldmeister" ["710"] + [("#START OF PROOF", "Proved Goals:")] [] Hypothesis Conjecture + [FOF] (K (250, ["poly_args"]) (* FUDGE *)) (* Setup *) @@ -436,7 +442,7 @@ Synchronized.change systems (fn _ => get_systems ()) val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp, - remote_tofof_e, remote_sine_e, remote_snark] + remote_tofof_e, remote_sine_e, remote_snark, remote_waldmeister] val setup = fold add_atp atps end;