--- a/src/Doc/Sledgehammer/document/root.tex Fri Sep 20 22:39:30 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Sep 20 22:39:30 2013 +0200
@@ -1298,6 +1298,11 @@
\optrueonly{dont\_compress\_isar}
Alias for ``\textit{isar\_compress} = 0''.
+\optrue{isar\_try0}
+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
+for the \keyw{try0} command.
\end{enum}
\subsection{Authentication}