# HG changeset patch
# User wenzelm
# Date 1288726306 -3600
# Node ID d4487353b3a0b9879090d876115a5ea497dc3f67
# Parent  132e2349694bfc21dc897b1c27d57a4b2e26a7e5
added convenience operation seconds: real -> time;

diff -r 132e2349694b -r d4487353b3a0 src/Pure/ML-Systems/timing.ML
--- a/src/Pure/ML-Systems/timing.ML	Tue Nov 02 20:16:56 2010 +0100
+++ b/src/Pure/ML-Systems/timing.ML	Tue Nov 02 20:31:46 2010 +0100
@@ -1,9 +1,11 @@
 (*  Title:      Pure/ML-Systems/timing.ML
     Author:     Makarius
 
-Compiler-independent timing functions.
+Basic support for timing.
 *)
 
+fun seconds s = Time.fromNanoseconds (Real.ceil (s * 1E9));
+
 fun start_timing () =
   let
     val real_timer = Timer.startRealTimer ();