# HG changeset patch
# User blanchet
# Date 1312875230 -7200
# Node ID bf489e54d7f8acc0e3ef4b4b3e1e2b54ed86e38f
# Parent  d40e5c72b346e6b2b7d9f063ac60648aad25e0c4
renamed E wrappers for consistency with CASC conventions

diff -r d40e5c72b346 -r bf489e54d7f8 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 09:33:01 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 09:33:50 2011 +0200
@@ -43,9 +43,9 @@
   val vampireN : string
   val leo2N : string
   val satallaxN : string
-  val sine_eN : string
+  val e_sineN : string
   val snarkN : string
-  val tofof_eN : string
+  val e_tofofN : string
   val waldmeisterN : string
   val z3_atpN : string
   val remote_prefix : string
@@ -108,9 +108,9 @@
 val z3_atpN = "z3_atp"
 val leo2N = "leo2"
 val satallaxN = "satallax"
-val sine_eN = "sine_e"
+val e_sineN = "e_sine"
 val snarkN = "snark"
-val tofof_eN = "tofof_e"
+val e_tofofN = "e_tofof"
 val waldmeisterN = "waldmeister"
 val remote_prefix = "remote_"
 
@@ -422,15 +422,15 @@
 val remote_satallax =
   remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
              (K (64, "simple_higher") (* FUDGE *))
-val remote_sine_e =
-  remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
+val remote_e_sine =
+  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
              Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
              [TFF, FOF] (K (100, "simple") (* FUDGE *))
-val remote_tofof_e =
-  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
+val remote_e_tofof =
+  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
              Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
@@ -462,7 +462,7 @@
 
 val atps =
   [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
-   remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
+   remote_leo2, remote_satallax, remote_e_sine, remote_snark, remote_e_tofof,
    remote_waldmeister]
 val setup = fold add_atp atps
 
diff -r d40e5c72b346 -r bf489e54d7f8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 09 09:33:01 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 09 09:33:50 2011 +0200
@@ -199,7 +199,7 @@
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put SPASS first. *)
 fun default_provers_param_value ctxt =
-  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, sine_eN, waldmeisterN]
+  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
                                   max_default_remote_threads)