diff -r d1c14898fd04 -r 03156257040f doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 03 20:19:24 2010 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 03 22:26:53 2010 +0100
@@ -378,9 +378,9 @@
 \textit{smart}.
 \item[$\bullet$] \qtybf{int\/}: An integer.
 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
-\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes),
-$s$ (seconds), or \textit{ms}
-(milliseconds), or the keyword \textit{none} ($\infty$ years).
+\item[$\bullet$] \qtybf{time}: An integer (e.g., 60) or floating-point number
+(e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
+($\infty$ seconds).
 \end{enum}
 
 Default values are indicated in square brackets. Boolean options have a negated
@@ -457,8 +457,8 @@
 \opnodefault{atp}{string}
 Legacy alias for \textit{provers}.
 
-\opdefault{timeout}{time}{$\mathbf{30}$ s}
-Specifies the maximum amount of time that the automatic provers should spend
+\opdefault{timeout}{time}{$\mathbf{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.