# HG changeset patch
# User blanchet
# Date 1320419158 0
# Node ID b9d5d3625e9a897460cd57a7d05a431f7f73131a
# Parent  2838109364f0f974990c1ffc61594fa0980603be
added remote iProver(-Eq) for experimentation

diff -r 2838109364f0 -r b9d5d3625e9a src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Nov 04 13:52:19 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Nov 04 15:05:58 2011 +0000
@@ -40,6 +40,8 @@
   val eN : string
   val e_sineN : string
   val e_tofofN : string
+  val iproverN : string
+  val iprover_eqN : string
   val leo2N : string
   val pffN : string
   val phfN : string
@@ -125,6 +127,8 @@
 val eN = "e"
 val e_sineN = "e_sine"
 val e_tofofN = "e_tofof"
+val iproverN = "iprover"
+val iprover_eqN = "iprover_eq"
 val leo2N = "leo2"
 val pffN = "pff"
 val phfN = "phf"
@@ -528,6 +532,12 @@
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
              Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *))
+val remote_iprover =
+  remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
+             (K (150, FOF, "mono_guards??") (* FUDGE *))
+val remote_iprover_eq =
+  remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
+             (K (150, FOF, "mono_guards??") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
@@ -565,8 +575,9 @@
 
 val atps =
   [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
-   remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine,
-   remote_snark, remote_e_tofof, remote_waldmeister]
+   remote_e_sine, remote_iprover, remote_iprover_eq, remote_leo2,
+   remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
+   remote_e_tofof, remote_waldmeister]
 val setup = fold add_atp atps
 
 end;