# 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;