# HG changeset patch
# User blanchet
# Date 1332345204 -3600
# Node ID 9f0b67fc07a8c5bfb7c887618da898e78712e947
# Parent  101976132929816c42675e0d05ddcf4b2bc0be4f
doc update

diff -r 101976132929 -r 9f0b67fc07a8 doc-src/Sledgehammer/sledgehammer.tex
--- 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