--- 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}