# HG changeset patch
# User blanchet
# Date 1407157693 -7200
# Node ID 913b5dd101cbd7e8f7e81973f01cdaca47488672
# Parent  2bf99b3f62e101c9e55d85beb228a6f1d57461af
updated 'compress' docs

diff -r 2bf99b3f62e1 -r 913b5dd101cb src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Aug 04 15:02:02 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Aug 04 15:08:13 2014 +0200
@@ -1272,13 +1272,16 @@
 one-line proofs. If the option is set to \textit{smart} (the default), Isar
 proofs are only generated when no working one-line proof is available.
 
-\opdefault{compress}{int}{\upshape 10}
+\opdefault{compress}{int}{smart}
 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.
+correspond to a group of up to $n$ consecutive proof steps in the ATP proof. If
+the option is set to \textit{smart} (the default), the compression factor is 10
+if the \textit{isar\_proofs} option is explicitly enabled; otherwise, it is
+$\infty$.
 
 \optrueonly{dont\_compress}
-Alias for ``\textit{compress} = 0''.
+Alias for ``\textit{compress} = 1''.
 
 \optrue{try0}{dont\_try0}
 Specifies whether standard proof methods such as \textit{auto} and