--- 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
@@ -1121,7 +1121,8 @@
\textit{overlord} (\S\ref{mode-of-operation}).}
\opdefault{max\_proofs}{int}{\upshape 4}
-Specifies the maximum number of proofs to display before stopping.
+Specifies the maximum number of proofs to display before stopping. This is a
+soft limit.
\opsmart{isar\_proofs}{no\_isar\_proofs}
Specifies whether Isar proofs should be output in addition to one-line proofs.