--- a/src/Doc/Sledgehammer/document/root.tex Wed Jul 09 11:54:01 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Jul 09 18:48:37 2014 +0200
@@ -872,19 +872,12 @@
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
-\item[\labelitemi] \textbf{\textit{metis}:} Although it is less powerful than
-the external provers, Metis itself can be used for proof search.
-
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
-\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt2} proof method with the
-current settings (usually:\ Z3 with proof reconstruction) can be used for proof
-search.
-
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
@@ -909,7 +902,6 @@
via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
> Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
a pre-release version of 4.3.2.
-\end{enum}
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
@@ -917,10 +909,11 @@
version 4.3.1 of Z3 or above. To use it, set the environment variable
\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp}
executable.
+\end{enum}
\end{sloppy}
-In addition to the local provers, the following remote provers are supported:
+Moreover, the following remote provers are supported:
\begin{enum}
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
@@ -980,6 +973,13 @@
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}.
+In addition to the local and remote provers, the Isabelle proof methods
+\textit{metis} and \textit{smt2} can be specified as \textbf{\textit{metis}}
+and \textbf{\textit{smt}}, respectively. They are generally not recommended
+for proof search but occasionally arise in Sledgehammer-generated
+minimization commands (e.g.,
+``\textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{metis}]'').
+
For the \textit{min} subcommand, the default prover is \textit{metis}. If
several provers are set, the first one is used.