# HG changeset patch
# User wenzelm
# Date 1288729267 -3600
# Node ID 2a33038d858b02ac97c79faff3b138d60b22a172
# Parent  bf39a257b3d38d1b3ff15622a525efaa8d807fb4
more on "Time" in Isabelle/ML;

diff -r bf39a257b3d3 -r 2a33038d858b doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Nov 02 20:55:12 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Nov 02 21:21:07 2010 +0100
@@ -1274,6 +1274,30 @@
 *}
 
 
+subsection {* Time *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML_type Time.time} \\
+  @{index_ML seconds: "real -> Time.time"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item Type @{ML_type 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 @{ML seconds}~@{text "s"} turns the concrete scalar @{text
+  "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}
+*}
+
+
 subsection {* Options *}
 
 text %mlref {*
diff -r bf39a257b3d3 -r 2a33038d858b doc-src/IsarImplementation/Thy/document/ML.tex
--- 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%