--- a/src/Doc/Sledgehammer/document/root.tex Thu Jan 30 14:28:04 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jan 30 14:37:53 2014 +0100
@@ -359,7 +359,7 @@
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
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}).
+\textit{compress\_isar} (\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
@@ -1303,15 +1303,15 @@
(the default), Isar proofs are only generated when no working one-liner
\textit{metis} proof is available.
-\opdefault{isar\_compress}{int}{\upshape 10}
+\opdefault{compress\_isar}{int}{\upshape 10}
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
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''.
+Alias for ``\textit{compress\_isar} = 0''.
-\optrue{isar\_try0}{dont\_try0\_isar}
+\optrue{try0\_isar}{dont\_try0\_isar}
Specifies whether standard proof methods such as \textit{auto} and
\textit{blast} should be tried as alternatives to \textit{metis} and
\textit{smt} in Isar proofs. The collection of methods is roughly the same as