--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 06 20:36:34 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 06 20:36:35 2011 +0200
@@ -492,30 +492,33 @@
set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
value or to try several provers and keep the nicest-looking proof.
-\point{What is metisFT?}
+\point{What are metisFT and metisX?}
The \textit{metisFT} proof method is the fully-typed version of Metis. It is
much slower than \textit{metis}, but the proof search is fully typed, and it
also includes more powerful rules such as the axiom ``$x = \mathit{True}
\mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places (e.g.,
-in set comprehensions). The method kicks in automatically as a fallback when
-\textit{metis} fails, and it is sometimes generated by Sledgehammer instead of
-\textit{metis} if the proof obviously requires type information or if
-\textit{metis} failed when Sledgehammer preplayed the proof. (By default,
-Sledgehammer tries to run \textit{metis} and/or \textit{metisFT} for 4 seconds
-to ensure that the generated one-line proofs actually work and to display timing
-information. This can be configured using the \textit{preplay\_timeout} option
-(\S\ref{timeouts}).)
+in set comprehensions).
+
+The \textit{metisX} proof method is an experimental version of Metis designed to
+subsume both \textit{metis} and \textit{metisFT}. The method kicks in
+automatically as a fallback when \textit{metis} fails, and it is sometimes
+generated by Sledgehammer instead of \textit{metis} if the proof obviously
+requires type information or if \textit{metis} failed when Sledgehammer
+preplayed the proof. (By default, Sledgehammer tries to run \textit{metis}
+and/or \textit{metisX} for 4 seconds to ensure that the generated one-line
+proofs actually work and to display timing information. This can be configured
+using the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
If you see the warning
\prew
\slshape
-Metis: Falling back on ``\textit{metisFT\/}''.
+Metis: Falling back on ``\textit{metisX\/}''.
\postw
in a successful Metis proof, you can advantageously replace the \textit{metis}
-call with \textit{metisFT}.
+call with \textit{metisX}.
\point{Are generated proofs minimal?}
@@ -751,6 +754,9 @@
the external provers, Metis itself can be used for proof search.
\item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis.
+
+\item[$\bullet$] \textbf{\textit{metisX}:} New experimental version of Metis,
+designed to subsume both \textit{metis} and \textit{metisFT}.
\end{enum}
In addition, the following remote provers are supported:
@@ -895,7 +901,7 @@
Like for \textit{poly\_preds} constants are annotated with their types to
resolve overloading, but otherwise no type information is encoded. This
coincides with the encoding used by the \textit{metis} command (before it falls
-back on \textit{metisFT}).
+back on \textit{metisX}).
\item[$\bullet$]
\textbf{%