diff -r bbed9f218158 -r d3c0734059ee src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Oct 24 22:05:57 2024 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 15:31:58 2024 +0200
@@ -59,16 +59,19 @@
 \Large A User's Guide to Sledgehammer for Isabelle/HOL}
 \author{\hbox{} \\
 Jasmin Blanchette \\
-{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]
+{\normalsize Institut f\"ur Informatik, Ludwig-Maximilians-Universit\"at M\"unchen} \\[4\smallskipamount]
 {\normalsize with contributions from} \\[4\smallskipamount]
 Martin Desharnais \\
 {\normalsize Forschungsinstitut CODE, Universit\"at der Bundeswehr M\"unchen}  \\[4\smallskipamount]
 Lawrence C. Paulson \\
-{\normalsize Computer Laboratory, University of Cambridge} \\
+{\normalsize Computer Laboratory, University of Cambridge} \\[4\smallskipamount]
+Lukas Bartl \\
+{\normalsize Institut f\"ur Informatik, Ludwig-Maximilians-Universit\"at M\"unchen} \\
 \hbox{}}
 
 \maketitle
 
+\newpage
 \tableofcontents
 
 \setlength{\parskip}{.7em plus .2em minus .1em}
@@ -313,7 +316,7 @@
 
 \point{Familiarize yourself with the main options}
 
-Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
+Sledgehammer's options are fully documented in \S\ref{option-reference}. Many of
 the options are very specialized, but serious users of the tool should at least
 familiarize themselves with the following options:
 
@@ -820,8 +823,8 @@
 Alias for \textit{provers}.
 
 \opsmartfalse{falsify}{dont\_falsify}
-Specifies whether Sledgehammer should look for falsifications or for proofs. By
-default, it looks for both.
+Specifies whether Sledgehammer should look for falsifications or for proofs. If
+the option is set to \textit{smart}, it looks for both.
 
 A falsification indicates that the goal, taken as an axiom, would be
 inconsistent with some specific background facts if it were added as a lemma,
@@ -836,10 +839,10 @@
 and found to be sufficient to prove the goal.
 
 Abduction is currently supported only by E. If the option is set to
-\textit{smart} (the default), abduction is enabled only in some of the E time
-slices, and at most one candidate missing assumption is displayed. You can
-disable abduction altogether by setting the option to 0 or enable it in all
-time slices by setting it to a nonzero value.
+\textit{smart}, abduction is enabled only in some of the E time slices, and at
+most one candidate missing assumption is displayed. You can disable abduction
+altogether by setting the option to 0 or enable it in all time slices by setting
+it to a nonzero value.
 
 \optrueonly{dont\_abduce}
 Alias for ``\textit{abduce} = 0''.
@@ -1199,12 +1202,26 @@
 
 \optrue{try0}{dont\_try0}
 Specifies whether standard proof methods such as \textit{auto} and
-\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
-The collection of methods is roughly the same as for the \textbf{try0} command.
+\textit{blast} should be tried as alternatives to \textit{metis} or
+\textit{smt}. The collection of methods is roughly the same as
+for the \textbf{try0} command.
 
 \optrue{smt\_proofs}{no\_smt\_proofs}
 Specifies whether the \textit{smt} proof method should be tried in addition to
 Isabelle's built-in proof methods.
+
+\opsmart{suggest\_of}{dont\_suggest\_of}
+Specifies whether Metis should try to infer variable instantiations before proof
+reconstruction, which results in instantiations of facts using \textbf{of}
+(e.g. \textit{map\_prod\_surj\_on}[\textbf{of} \textit{f A} "\textit{f}
+\textasciigrave \textit{A}" \textit{g B} "\textit{g} \textasciigrave
+\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}