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