src/Pure/ML-Systems/timing.ML
2009-10-14 wenzelm 2009-10-14 show direct GC time (which is included in CPU time);
2009-06-22 wenzelm 2009-06-22 end_timing: checked divisions with sane defaults;
2009-06-17 wenzelm 2009-06-17 end_timing: actually display GC percentage, not factor;
2009-06-17 wenzelm 2009-06-17 more detailed start_timing/end_timing (in timing.ML); removed obsolete check_timer;