--- a/src/Doc/Sledgehammer/document/root.tex Tue Oct 29 10:26:06 2024 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Oct 31 09:24:10 2024 +0100
@@ -630,6 +630,9 @@
\item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}.
\end{enum}
+The \textit{metis} method also supports the Isabelle option
+[[\textit{metis\_suggest\_of}]], which tells \textit{metis} to suggest
+instantiations of facts using \textbf{of} from a successful proof.
\section{Option Reference}
\label{option-reference}
@@ -1218,10 +1221,6 @@
\textit{B}"]). This can make the proof methods faster and more intelligible. If
the option is set to \textit{smart} (the default), variable instantiations are
inferred only if proof reconstruction failed or timed out.
-
-When using \textit{metis} directly, enable the configuration
-option [[\textit{metis\_suggest\_of}]] to directly get a suggestion with
-instantiations of facts using \textbf{of} from a successful proof.
\end{enum}