--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 07:57:24 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 08:52:35 2011 +0200
@@ -495,30 +495,35 @@
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 is the \textit{full\_types}/\textit{no\_types} argument to Metis?}
-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}).)
+The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed
+version of Metis. It is somewhat 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} with
+various options for up to 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{metis} (\textit{full\_types})''.
\postw
-in a successful Metis proof, you can advantageously replace the \textit{metis}
-call with \textit{metisFT}.
+in a successful Metis proof, you can advantageously pass the
+\textit{full\_types} option to \textit{metis} directly.
+
+At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
+uses no type information at all during the proof search, which is more efficient
+but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
+generated by Sledgehammer.
\point{Are generated proofs minimal?}
@@ -664,8 +669,8 @@
Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and
\qty{facts} is a list of arbitrary facts. \qty{type\_sys} may also be
\textit{full\_types}, in which case an appropriate type-sound encoding is
-chosen. The companion proof method \textit{metisFT} is an abbreviation for
-``\textit{metis}~(\textit{full\_types})''.
+chosen, \textit{partial\_types} (the default), or \textit{no\_types}, a synonym
+for \textit{erased}.
\section{Option Reference}
\label{option-reference}
@@ -764,7 +769,11 @@
\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
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{metis\_full\_types}:} Fully typed version of
+Metis, corresponding to \textit{metis} (\textit{full\_types}).
+
+\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
+corresponding to \textit{metis} (\textit{no\_types}).
\end{enum}
In addition, the following remote provers are supported:
@@ -903,14 +912,12 @@
arguments, to resolve overloading.
\item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
-tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. This
-coincides with the encoding used by the \textit{metisFT} command.
+tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
\item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
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}).
+coincides with the default encoding used by the \textit{metis} command.
\item[$\bullet$]
\textbf{%