--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 06 20:36:35 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 06 20:36:35 2011 +0200
@@ -492,33 +492,30 @@
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 are metisFT and metisX?}
+\point{What is metisFT?}
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 \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}).)
+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}).)
If you see the warning
\prew
\slshape
-Metis: Falling back on ``\textit{metisX\/}''.
+Metis: Falling back on ``\textit{metisFT\/}''.
\postw
in a successful Metis proof, you can advantageously replace the \textit{metis}
-call with \textit{metisX}.
+call with \textit{metisFT}.
\point{Are generated proofs minimal?}
@@ -901,7 +898,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{metisX}).
+back on \textit{metisFT}).
\item[$\bullet$]
\textbf{%