1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Sep 22 18:23:38 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Sep 22 19:42:06 2011 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
     1.5  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
     1.6  \texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
     1.7 -with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
     1.8 +with E 1.0 to 1.4, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
     1.9  \footnote{Following the rewrite of Vampire, the counter for version numbers was
    1.10  reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
    1.11  than, say, Vampire 9.0 or 11.5.}%
    1.12 @@ -265,16 +265,12 @@
    1.13  $[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.14  Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
    1.15  %
    1.16 -Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\
    1.17 -$[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.18 -Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
    1.19 -%
    1.20  Sledgehammer: ``\textit{remote\_z3}'' on goal \\
    1.21  $[a] = [b] \,\Longrightarrow\, a = b$ \\
    1.22  Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
    1.23  \postw
    1.24  
    1.25 -Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
    1.26 +Sledgehammer ran E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
    1.27  Depending on which provers are installed and how many processor cores are
    1.28  available, some of the provers might be missing or present with a
    1.29  \textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
    1.30 @@ -505,7 +501,7 @@
    1.31  Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
    1.32  \postw
    1.33  
    1.34 -in a successful Metis proof, you can advantageously pass the
    1.35 +for a successful Metis proof, you can advantageously pass the
    1.36  \textit{full\_types} option to \textit{metis} directly.
    1.37  
    1.38  \point{Are generated proofs minimal?}
    1.39 @@ -818,7 +814,7 @@
    1.40  with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
    1.41  \end{enum}
    1.42  
    1.43 -By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
    1.44 +By default, Sledgehammer runs E, SPASS, Vampire, Z3 (or whatever
    1.45  the SMT module's \textit{smt\_solver} configuration option is set to), and (if
    1.46  appropriate) Waldmeister in parallel---either locally or remotely, depending on
    1.47  the number of processor cores available. For historical reasons, the default

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Sep 22 18:23:38 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Sep 22 19:42:06 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, e_sineN, waldmeisterN]
     2.8 +  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, 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)