--- 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}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 19 19:44:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Feb 20 08:44:24 2013 +0100
@@ -102,7 +102,8 @@
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
- ("dont_preplay", ("preplay_timeout", ["0"]))]
+ ("dont_preplay", ("preplay_timeout", ["0"])),
+ ("dont_compress_isar", ("compress_isar", ["0"]))]
val negated_alias_params =
[("no_debug", "debug"),
("quiet", "verbose"),