| Sun, 20 Mar 2011 21:44:38 +0100 | wenzelm | pure Timing.timing, without any exception handling; | changeset | files |
| Sun, 20 Mar 2011 21:28:11 +0100 | wenzelm | structure Timing: covers former start_timing/end_timing and Output.timeit etc; | changeset | files |
| Sun, 20 Mar 2011 21:20:07 +0100 | wenzelm | pervasive cond_timeit; | changeset | files |