# HG changeset patch
# User blanchet
# Date 1361346264 -3600
# Node ID a55ef201b19d6aa429c297a17ab6fed598ff913e
# Parent  9b5bf1a9a710b89d5585a315f4c6b9680f6b5808
alias for people like me

diff -r 9b5bf1a9a710 -r a55ef201b19d src/Doc/Sledgehammer/document/root.tex
--- 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}
diff -r 9b5bf1a9a710 -r a55ef201b19d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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"),