src/Doc/Sledgehammer/document/root.tex

 For each successful prover, Sledgehammer gives a one-liner \textit{metis} or
 \textit{smt} method call. Rough timings are shown in parentheses, indicating how
 fast the call is. You can click the proof to insert it into the theory text.
 
 In addition, you can ask Sledgehammer for an Isar text proof by passing the
-\textit{isar\_proof} option (\S\ref{output-format}):
-
-\prew
-\textbf{sledgehammer} [\textit{isar\_proof}]
+\textit{isar\_proofs} option (\S\ref{output-format}):
+
+\prew
+\textbf{sledgehammer} [\textit{isar\_proofs}]
 \postw
 
 When Isar proof construction is successful, it can yield proofs that are more
 readable and also faster than the \textit{metis} or \textit{smt} one-liners.
 This feature is experimental and is only available for ATPs.

 specifies the maximum number of facts that should be passed to the provers. By
 default, the value is prover-dependent but varies between about 50 and 1000. If
 the provers time out, you can try lowering this value to, say, 25 or 50 and see
 if that helps.
 
-\item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
+\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
 that Isar proofs should be generated, instead of one-liner \textit{metis} or
 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
-\textit{isar\_shrink\_factor} (\S\ref{output-format}).
+\textit{isar\_shrinkage} (\S\ref{output-format}).
 
 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
 asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
 if you are the kind of user who can think clearly while ATPs are active.

 proof is too difficult for it. Metis's search is complete, so it should
 eventually find it, but that's little consolation. There are several possible
 solutions:
 
 \begin{enum}
-\item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
+\item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to
 obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
 Since the steps are fairly small, \textit{metis} is more likely to be able to
 replay them.
 
 \item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}.

 strongly encouraged to report this to the author at \authoremail.
 
 \point{Why are the generated Isar proofs so ugly/broken?}
 
 The current implementation of the Isar proof feature,
-enabled by the \textit{isar\_proof} option (\S\ref{output-format}),
+enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
 is highly experimental. Work on a new implementation has begun. There is a large body of
 research into transforming resolution proofs into natural deduction proofs (such
 as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
-set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
+set the \textit{isar\_shrinkage} option (\S\ref{output-format}) to a larger
 value or to try several provers and keep the nicest-looking proof.
 
 \point{How can I tell whether a suggested proof is sound?}
 
 Earlier versions of Sledgehammer often suggested unsound proofs---either proofs

 \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
 \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For
 example:
 
 \prew
-\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120]
+\textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120]
 \postw
 
 Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
 
 \prew

 automatic runs.
 
 \nopagebreak
 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
 
-\opfalse{isar\_proof}{no\_isar\_proof}
+\opfalse{isar\_proofs}{no\_isar\_proofs}
 Specifies whether Isar proofs should be output in addition to one-liner
 \textit{metis} proofs. Isar proof construction is still experimental and often
 fails; however, they are usually faster and sometimes more robust than
 \textit{metis} proofs.
 
-\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
-Specifies the granularity of the Isar proof. A value of $n$ indicates that each
-Isar proof step should correspond to a group of up to $n$ consecutive proof
-steps in the ATP proof.
+\opdefault{isar\_shrinkage}{int}{\upshape 10}
+Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
+is enabled. A value of $n$ indicates that each Isar proof step should correspond
+to a group of up to $n$ consecutive proof steps in the ATP proof.
 \end{enum}
 
 \subsection{Authentication}
 \label{authentication}