# HG changeset patch
# User blanchet
# Date 1316713326 -7200
# Node ID 59ca831deef485901823c139d372e81bf3e638de
# Parent  3aa8d3c391a4f63f910dd8ecbbf4ecbe08969675
take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime

diff -r 3aa8d3c391a4 -r 59ca831deef4 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Sep 22 18:23:38 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Sep 22 19:42:06 2011 +0200
@@ -176,7 +176,7 @@
 set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
 \texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
-with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
+with E 1.0 to 1.4, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
 reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
 than, say, Vampire 9.0 or 11.5.}%
@@ -265,16 +265,12 @@
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
-%
 Sledgehammer: ``\textit{remote\_z3}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
 \postw
 
-Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
 Depending on which provers are installed and how many processor cores are
 available, some of the provers might be missing or present with a
 \textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
@@ -505,7 +501,7 @@
 Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
 \postw
 
-in a successful Metis proof, you can advantageously pass the
+for a successful Metis proof, you can advantageously pass the
 \textit{full\_types} option to \textit{metis} directly.
 
 \point{Are generated proofs minimal?}
@@ -818,7 +814,7 @@
 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
-By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
+By default, Sledgehammer runs E, SPASS, Vampire, Z3 (or whatever
 the SMT module's \textit{smt\_solver} configuration option is set to), and (if
 appropriate) Waldmeister in parallel---either locally or remotely, depending on
 the number of processor cores available. For historical reasons, the default
diff -r 3aa8d3c391a4 -r 59ca831deef4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Sep 22 18:23:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Sep 22 19:42:06 2011 +0200
@@ -201,7 +201,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, e_sineN, waldmeisterN]
+  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, waldmeisterN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
                                   max_default_remote_threads)