src/Doc/Sledgehammer/document/root.tex

 
 \nopagebreak
 {\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;
 however, when they succeed they are usually faster and more intelligible than
 one-line proofs. If the option is set to \textit{smart} (the default), Isar