src/Doc/Sledgehammer/document/root.tex

 
 \opdefault{isar\_compress}{int}{\upshape 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}
 \label{authentication}