author | wenzelm |
Thu, 04 Nov 2010 10:22:59 +0100 | |
changeset 40336 | 755862729f8d |
parent 40335 | 3e4bb6e7c3ca |
child 40337 | d25bbb5f1c9e |
--- 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