src/Pure/General/timing.ML
Sat, 06 Nov 2010 17:55:32 +0100 wenzelm somewhat more uniform timing in ML vs. Scala;
less more (0) tip