--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Mar 21 16:53:24 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Mar 21 16:53:24 2012 +0100
@@ -282,12 +282,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 \\
+Sledgehammer: ``\textit{remote\_satallax\/}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
\postw
-Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, Satallax, 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,
@@ -858,8 +858,8 @@
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
-developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
-E-SInE runs on Geoff Sutcliffe's Miami servers.
+developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff
+Sutcliffe's Miami servers.
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
@@ -905,7 +905,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, Satallax, 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