# HG changeset patch
# User blanchet
# Date 1428512308 -7200
# Node ID 4c51341245a1013f465d4dcc65a713612020f374
# Parent  b622365f181cfc7d1320a2809b836cd97533c9f8
updated docs to reflect actually run ATPs

diff -r b622365f181c -r 4c51341245a1 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Apr 08 18:55:52 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Apr 08 18:58:28 2015 +0200
@@ -259,27 +259,22 @@
 
 \prew
 \slshape
-Sledgehammer: ``\textit{e\/}'' \\
+Sledgehammer: ``\textit{cvc4\/}'' \\
 Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{z3\/}'' \\
 Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{vampire\/}'' \\
+Sledgehammer: ``\textit{remote\_vampire\/}'' \\
 Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{spass\/}'' \\
 Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
-%
-Sledgehammer: ``\textit{remote\_e\_sine\/}'' \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
 \postw
 
-Sledgehammer ran E, E-SInE, SPASS, Vampire, 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, where the goal's
-conclusion is a (universally quantified) equation.
+Sledgehammer ran CVC4, SPASS, Vampire, 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.
 
 For each successful prover, Sledgehammer gives a one-line \textit{metis} or
 \textit{smt2} method call. Rough timings are shown in parentheses, indicating how