1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Sep 23 14:25:53 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Sep 23 16:44:51 2011 +0200
     1.3 @@ -265,12 +265,16 @@
     1.4  $[a] = [b] \,\Longrightarrow\, a = b$ \\
     1.5  Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
     1.6  %
     1.7 +Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\
     1.8 +$[a] = [b] \,\Longrightarrow\, a = b$ \\
     1.9 +Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
    1.10 +%
    1.11  Sledgehammer: ``\textit{remote\_z3}'' on goal \\
    1.12  $[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.13  Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
    1.14  \postw
    1.15  
    1.16 -Sledgehammer ran E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
    1.17 +Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
    1.18  Depending on which provers are installed and how many processor cores are
    1.19  available, some of the provers might be missing or present with a
    1.20  \textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
    1.21 @@ -814,7 +818,7 @@
    1.22  with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
    1.23  \end{enum}
    1.24  
    1.25 -By default, Sledgehammer runs E, SPASS, Vampire, Z3 (or whatever
    1.26 +By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
    1.27  the SMT module's \textit{smt\_solver} configuration option is set to), and (if
    1.28  appropriate) Waldmeister in parallel---either locally or remotely, depending on
    1.29  the number of processor cores available. For historical reasons, the default

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 23 14:25:53 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 23 16:44:51 2011 +0200
     2.3 @@ -201,7 +201,7 @@
     2.4  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
     2.5     timeout, it makes sense to put SPASS first. *)
     2.6  fun default_provers_param_value ctxt =
     2.7 -  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, waldmeisterN]
     2.8 +  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
     2.9    |> map_filter (remotify_prover_if_not_installed ctxt)
    2.10    |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
    2.11                                    max_default_remote_threads)