--- a/doc-src/Sledgehammer/sledgehammer.tex Thu May 19 10:24:13 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu May 19 10:24:13 2011 +0200
@@ -324,10 +324,10 @@
\item[$\bullet$] \textbf{\textit{provers}} specifies the ATP and SMT solvers to
use (e.g., ``\textit{provers} = \textit{e spass remote\_vampire}'').
-\item[$\bullet$] \textbf{\textit{timeout}} controls the time limit. It is set to
-30 seconds, but since Sledgehammer runs asynchronously you should not hesitate
-to crank up this limit to 60 or 120 seconds if you are the kind of user who can
-think clearly while ATPs are active.
+\item[$\bullet$] \textbf{\textit{timeout}} controls the provers' time limit. It
+is set to 30 seconds, but since Sledgehammer runs asynchronously you should not
+hesitate to raise this limit to 60 or 120 seconds if you are the kind of user
+who can think clearly while ATPs are active.
\item[$\bullet$] \textbf{\textit{full\_types}} specifies whether type-sound
encodings should be used. By default, Sledgehammer employs a mixture of
@@ -428,6 +428,10 @@
% to re-find by Metis
% * but the opposite is sometimes the case
+% Why is Sledgehammer automatically minimizing sometimes?
+% * some provers (e.g. CVC3 and Yices)
+% * also, sometimes E finds a proof but doesn't give a proof object
+
\point{I got a strange error from Sledgehammer---what should I do?}
Sledgehammer tries to give informative error messages. Please report any strange
@@ -678,9 +682,10 @@
\opdefault{timeout}{float\_or\_none}{\upshape 30}
Specifies the maximum number of seconds that the automatic provers should spend
-searching for a proof. For historical reasons, the default value of this option
-can be overridden using the option ``Sledgehammer: Time Limit'' from the
-``Isabelle'' menu in Proof General.
+searching for a proof. This excludes problem preparation and is a soft limit.
+For historical reasons, the default value of this option can be overridden using
+the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof
+General.
\opfalse{blocking}{non\_blocking}
Specifies whether the \textbf{sledgehammer} command should operate