# HG changeset patch
# User blanchet
# Date 1379709570 -7200
# Node ID 7bb0cf27c2436298a1041be630b8190d09150e6f
# Parent  eba0d1c069b8938a8e8a53838571fab144b511bc
document option

diff -r eba0d1c069b8 -r 7bb0cf27c243 src/Doc/Sledgehammer/document/root.tex
--- 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}