--- a/src/Doc/Sledgehammer/document/root.tex Tue Feb 19 19:44:10 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Feb 20 08:44:24 2013 +0100
@@ -1306,6 +1306,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.
+
+\optrueonly{dont\_compress\_isar}
+Alias for ``\textit{isar\_compress} = 0''.
+
\end{enum}
\subsection{Authentication}