--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Nov 02 20:55:12 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Nov 02 21:21:07 2010 +0100
@@ -1643,6 +1643,44 @@
%
\endisadelimmlref
%
+\isamarkupsubsection{Time%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML type}{Time.time}\verb|type Time.time| \\
+ \indexdef{}{ML}{seconds}\verb|seconds: real -> Time.time| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item Type \verb|Time.time| represents time abstractly according
+ to the SML97 basis library definition. This is adequate for
+ internal ML operations, but awkward in concrete time specifications.
+
+ \item \verb|seconds|~\isa{s} turns the concrete scalar \isa{s} (measured in seconds) into an abstract time value. Floating
+ point numbers are easy to use as context parameters (e.g.\ via
+ configuration options, see \secref{sec:config-options}) or
+ preferences that are maintained by external tools as well.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsubsection{Options%
}
\isamarkuptrue%