# 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