changeset 40336 | 755862729f8d |
parent 40300 | d4487353b3a0 |
child 40391 | b0dafbfc05b7 |
--- a/src/Pure/ML-Systems/timing.ML Wed Nov 03 21:53:56 2010 +0100 +++ b/src/Pure/ML-Systems/timing.ML Thu Nov 04 10:22:59 2010 +0100 @@ -1,10 +1,10 @@ (* Title: Pure/ML-Systems/timing.ML Author: Makarius -Basic support for timing. +Basic support for time measurement. *) -fun seconds s = Time.fromNanoseconds (Real.ceil (s * 1E9)); +val seconds = Time.fromReal; fun start_timing () = let