author blanchet Mon, 04 Aug 2014 15:08:13 +0200 changeset 57784 913b5dd101cb parent 57783 2bf99b3f62e1 child 57785 0388026060d1
updated 'compress' docs
--- 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