# HG changeset patch
# User blanchet
# Date 1316789091 -7200
# Node ID b3b50d8b535a81be1ef268437059be8eaf65fd1d
# Parent  9598cada31b351ceb57e16dd68acffd8bb763904
reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)

diff -r 9598cada31b3 -r b3b50d8b535a doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Sep 23 14:25:53 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Sep 23 16:44:51 2011 +0200
@@ -265,12 +265,16 @@
 $[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, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, E-SInE, 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,
@@ -814,7 +818,7 @@
 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
-By default, Sledgehammer runs E, SPASS, Vampire, Z3 (or whatever
+By default, Sledgehammer runs E, E-SInE, 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 9598cada31b3 -r b3b50d8b535a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 23 14:25:53 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 23 16:44:51 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, 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)