--- a/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
@@ -1120,6 +1120,9 @@
{\small See also \textit{spy} (\S\ref{mode-of-operation}) and
\textit{overlord} (\S\ref{mode-of-operation}).}
+\opdefault{max\_proofs}{int}{\upshape 4}
+Specifies the maximum number of proofs to display before stopping.
+
\opsmart{isar\_proofs}{no\_isar\_proofs}
Specifies whether Isar proofs should be output in addition to one-line proofs.
The construction of Isar proof is still experimental and may sometimes fail;