--- a/src/Doc/Sledgehammer/document/root.tex Wed Feb 20 08:44:24 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Feb 20 08:44:24 2013 +0100
@@ -308,7 +308,7 @@
\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
+In addition, you can ask Sledgehammer for an Isar text proof by enabling the
\textit{isar\_proofs} option (\S\ref{output-format}):
\prew
@@ -367,7 +367,7 @@
if that helps.
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
-that Isar proofs should be generated, instead of one-liner \textit{metis} or
+that Isar proofs should be generated, in addition to one-liner \textit{metis} or
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
\textit{isar\_compress} (\S\ref{output-format}).
@@ -501,15 +501,15 @@
using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
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\_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\_compress} option (\S\ref{output-format}) to a larger
-value or to try several provers and keep the nicest-looking proof.
+%\point{Why are the generated Isar proofs so ugly/broken?}
+%
+%The current implementation of the Isar proof feature,
+%enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
+%is 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\_compress} 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?}
@@ -1296,16 +1296,18 @@
\nopagebreak
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
-\opfalse{isar\_proofs}{no\_isar\_proofs}
+\opsmart{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.
+\textit{metis} 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 \textit{metis} proofs. If the option is set to \textit{smart}
+(the default), Isar proofs are only generated when no working one-liner
+\textit{metis} proof is available.
\opdefault{isar\_compress}{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.
+is explicitly 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.
\optrueonly{dont\_compress\_isar}
Alias for ``\textit{isar\_compress} = 0''.