# HG changeset patch
# User blanchet
# Date 1423662696 -3600
# Node ID b1c1f6f9a2124055fbc0ce3046df34c1606649fc
# Parent  dd9a5c7663cbfe1b7993594b2c14819f35d76213
updated Sledgehammer docs

diff -r dd9a5c7663cb -r b1c1f6f9a212 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Feb 11 14:48:07 2015 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Feb 11 14:51:36 2015 +0100
@@ -164,7 +164,7 @@
 \begin{sloppy}
 \begin{enum}
 \item[\labelitemi] If you installed an official Isabelle package, it should
-already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
+already include properly setup executables for CVC4, E, SPASS, and Z3, ready to use.%
 \footnote{Vampire's license prevents us from doing the same for
 this otherwise remarkable tool.}
 For Z3, you must additionally set the variable
@@ -174,13 +174,14 @@
 via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
 > Isabelle > General'' in Isabelle/jEdit.
 
-\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
-SPASS, and Z3 binary packages from \download. Extract the archives, then add a
-line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
+\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
+CVC4, E, SPASS, and Z3 binary packages from \download. Extract the archives,
+then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash
+components}%
 \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
 startup. Its value can be retrieved by executing \texttt{isabelle}
 \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
-file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
+file with the absolute path to CVC3, CVC4, E, SPASS, or Z3. For example, if the
 \texttt{components} file does not exist yet and you extracted SPASS to
 \texttt{/usr/local/spass-3.8ds}, create it with the single line
 
@@ -942,13 +943,10 @@
 runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
-By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
-and Z3 in parallel---either locally or remotely, depending on the number of
-processor cores available.
-
-It is generally a good idea to run several provers in parallel. Running E,
-SPASS, and Vampire for 5~seconds yields a similar success rate to running the
-most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
+By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire,
+veriT, and Z3 in parallel---either locally or remotely, depending on the number
+of processor cores available and on which provers are actually installed.
+It is generally a good idea to run several provers in parallel.
 
 \opnodefault{prover}{string}
 Alias for \textit{provers}.