src/Pure/ML-Systems/timing.ML
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;