src/Pure/General/timing.ML
Wed, 24 Aug 2011 15:30:43 +0200 wenzelm ignore irrelevant timings;
Sun, 15 May 2011 20:50:22 +0200 wenzelm only show relevant timing;
Mon, 21 Mar 2011 20:15:03 +0100 wenzelm tuned;
Sun, 20 Mar 2011 21:44:38 +0100 wenzelm pure Timing.timing, without any exception handling;
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Sat, 06 Nov 2010 17:55:32 +0100 wenzelm somewhat more uniform timing in ML vs. Scala;
less more (0) tip