# HG changeset patch
# User blanchet
# Date 1506804923 -7200
# Node ID 5887ae5b95a805b2c9f23f9807f8f22a4b9ae517
# Parent  ea5bd1347d26edeb40e5a73857ebfdc351ddf278
updated Sledgehammer docs

diff -r ea5bd1347d26 -r 5887ae5b95a8 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Sat Sep 30 22:55:16 2017 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Sat Sep 30 22:55:23 2017 +0200
@@ -165,9 +165,7 @@
 \begin{sloppy}
 \begin{enum}
 \item[\labelitemi] If you installed an official Isabelle package, it should
-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.}
+already include properly setup executables for CVC4, E, SPASS, veriT, and Z3, ready to use.
 
 \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
 CVC4, E, SPASS, and Z3 binary packages from \download. Extract the archives,
@@ -186,26 +184,26 @@
 
 in it.
 
-\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II,
-Satallax, or SPASS manually, or found a Vampire executable somewhere (e.g.,
+\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, or
+Satallax manually, or found a Vampire executable somewhere (e.g.,
 \url{http://www.vprover.org/}), set the environment variable
 \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
-\texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
+\texttt{SATALLAX\_HOME}, or
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL},
 \texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
-\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable;
+\texttt{leo}, \texttt{satallax}, or \texttt{vampire} executable;
 for Alt-Ergo, set the
 environment variable \texttt{WHY3\_HOME} to the directory that contains the
 \texttt{why3} executable.
 Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0,
-LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 4.0.%
+LEO-II 1.3.4, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
 reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
 recent than 9.0 or 11.5.}%
 Since the ATPs' output formats are neither documented nor stable, other
 versions might not work well with Sledgehammer. Ideally,
 you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
-\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
+\texttt{SATALLAX\_VERSION}, or
 \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0'').
 
 Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
@@ -220,11 +218,11 @@
 \end{enum}
 \end{sloppy}
 
-To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try
-out the example in \S\ref{first-steps}. If the remote versions of any of these
-provers is used (identified by the prefix ``\textit{remote\_\/}''), or if the
-local versions fail to solve the easy goal presented there, something must be
-wrong with the installation.
+To check whether the provers are successfully installed, try out the example
+in \S\ref{first-steps}. If the remote versions of any of these provers is used
+(identified by the prefix ``\textit{remote\_\/}''), or if the local versions
+fail to solve the easy goal presented there, something must be wrong with the
+installation.
 
 Remote prover invocation requires Perl with the World Wide Web Library
 (\texttt{libwww-perl}) installed. If you must use a proxy server to access the
@@ -312,11 +310,6 @@
 is better for first-order problems. Hence, you may get better results if you
 first simplify the problem to remove higher-order features.
 
-\point{Make sure E, SPASS, Vampire, and Z3 are locally installed}
-
-Locally installed provers are faster and more reliable than those running on
-servers. See \S\ref{installation} for details on how to install them.
-
 \point{Familiarize yourself with the main options}
 
 Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
@@ -591,8 +584,8 @@
 theory to process all the available facts, learning from proofs generated by
 automatic provers. The prover to use and its timeout can be set using the
 \textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
-(\S\ref{timeouts}) options. It is recommended to perform learning using an
-efficient first-order ATP (such as E, SPASS, and Vampire) as opposed to a
+(\S\ref{timeouts}) options. It is recommended to perform learning using a
+first-order ATP (such as E, SPASS, and Vampire) as opposed to a
 higher-order ATP or an SMT solver.
 
 \item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}