# HG changeset patch
# User blanchet
# Date 1350565849 -7200
# Node ID 54ec43352eb1c790a7c220b620186248329610ca
# Parent  cf441f4a358bbd66df109b49c43f4a824e44ef74
updated docs

diff -r cf441f4a358b -r 54ec43352eb1 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Oct 18 15:05:17 2012 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Oct 18 15:10:49 2012 +0200
@@ -309,10 +309,10 @@
 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}):
+\textit{isar\_proofs} option (\S\ref{output-format}):
 
 \prew
-\textbf{sledgehammer} [\textit{isar\_proof}]
+\textbf{sledgehammer} [\textit{isar\_proofs}]
 \postw
 
 When Isar proof construction is successful, it can yield proofs that are more
@@ -366,10 +366,10 @@
 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
@@ -470,7 +470,7 @@
 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.
@@ -504,11 +504,11 @@
 \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?}
@@ -723,7 +723,7 @@
 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}:
@@ -1293,16 +1293,16 @@
 \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}