--- 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}