--- a/src/Doc/Sledgehammer/document/root.tex Tue Oct 01 17:06:35 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Oct 01 19:58:31 2013 +0200
@@ -1311,7 +1311,7 @@
\optrueonly{dont\_compress\_isar}
Alias for ``\textit{isar\_compress} = 0''.
-\optrue{isar\_try0}
+\optrue{isar\_try0}{dont\_try0\_isar}
Specifies whether standard proof methods such as \textit{auto} and
\textit{blast} should be tried as alternatives to \textit{metis} and
\textit{smt} in Isar proofs. The collection of methods is roughly the same as