1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Thu Oct 18 15:05:17 2012 +0200
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Thu Oct 18 15:10:49 2012 +0200
     1.3 @@ -309,10 +309,10 @@
     1.4  fast the call is. You can click the proof to insert it into the theory text.
     1.5  
     1.6  In addition, you can ask Sledgehammer for an Isar text proof by passing the
     1.7 -\textit{isar\_proof} option (\S\ref{output-format}):
     1.8 +\textit{isar\_proofs} option (\S\ref{output-format}):
     1.9  
    1.10  \prew
    1.11 -\textbf{sledgehammer} [\textit{isar\_proof}]
    1.12 +\textbf{sledgehammer} [\textit{isar\_proofs}]
    1.13  \postw
    1.14  
    1.15  When Isar proof construction is successful, it can yield proofs that are more
    1.16 @@ -366,10 +366,10 @@
    1.17  the provers time out, you can try lowering this value to, say, 25 or 50 and see
    1.18  if that helps.
    1.19  
    1.20 -\item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
    1.21 +\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
    1.22  that Isar proofs should be generated, instead of one-liner \textit{metis} or
    1.23  \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
    1.24 -\textit{isar\_shrink\_factor} (\S\ref{output-format}).
    1.25 +\textit{isar\_shrinkage} (\S\ref{output-format}).
    1.26  
    1.27  \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
    1.28  provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
    1.29 @@ -470,7 +470,7 @@
    1.30  solutions:
    1.31  
    1.32  \begin{enum}
    1.33 -\item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
    1.34 +\item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to
    1.35  obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
    1.36  Since the steps are fairly small, \textit{metis} is more likely to be able to
    1.37  replay them.
    1.38 @@ -504,11 +504,11 @@
    1.39  \point{Why are the generated Isar proofs so ugly/broken?}
    1.40  
    1.41  The current implementation of the Isar proof feature,
    1.42 -enabled by the \textit{isar\_proof} option (\S\ref{output-format}),
    1.43 +enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
    1.44  is highly experimental. Work on a new implementation has begun. There is a large body of
    1.45  research into transforming resolution proofs into natural deduction proofs (such
    1.46  as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
    1.47 -set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
    1.48 +set the \textit{isar\_shrinkage} option (\S\ref{output-format}) to a larger
    1.49  value or to try several provers and keep the nicest-looking proof.
    1.50  
    1.51  \point{How can I tell whether a suggested proof is sound?}
    1.52 @@ -723,7 +723,7 @@
    1.53  example:
    1.54  
    1.55  \prew
    1.56 -\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120]
    1.57 +\textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120]
    1.58  \postw
    1.59  
    1.60  Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
    1.61 @@ -1293,16 +1293,16 @@
    1.62  \nopagebreak
    1.63  {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
    1.64  
    1.65 -\opfalse{isar\_proof}{no\_isar\_proof}
    1.66 +\opfalse{isar\_proofs}{no\_isar\_proofs}
    1.67  Specifies whether Isar proofs should be output in addition to one-liner
    1.68  \textit{metis} proofs. Isar proof construction is still experimental and often
    1.69  fails; however, they are usually faster and sometimes more robust than
    1.70  \textit{metis} proofs.
    1.71  
    1.72 -\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
    1.73 -Specifies the granularity of the Isar proof. A value of $n$ indicates that each
    1.74 -Isar proof step should correspond to a group of up to $n$ consecutive proof
    1.75 -steps in the ATP proof.
    1.76 +\opdefault{isar\_shrinkage}{int}{\upshape 10}
    1.77 +Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
    1.78 +is enabled. A value of $n$ indicates that each Isar proof step should correspond
    1.79 +to a group of up to $n$ consecutive proof steps in the ATP proof.
    1.80  \end{enum}
    1.81  
    1.82  \subsection{Authentication}