src/Pure/General/timing.ML
2011-03-20 ago structure Timing: covers former start_timing/end_timing and Output.timeit etc;
2010-11-06 ago somewhat more uniform timing in ML vs. Scala;