| changeset 74158 | 1cb0ad6f9a2d |
| parent 67932 | 04352338f7f3 |
| child 78705 | fde0b195cb7d |
| 74156:ecf80e37ed1a | 74158:1cb0ad6f9a2d |
|---|---|
1 (* Title: Pure/General/timing.ML |
1 (* Title: Pure/General/timing.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Basic support for time measurement. |
4 Support for time measurement. |
5 *) |
5 *) |
6 |
6 |
7 signature BASIC_TIMING = |
7 signature BASIC_TIMING = |
8 sig |
8 sig |
9 val cond_timeit: bool -> string -> (unit -> 'a) -> 'a |
9 val cond_timeit: bool -> string -> (unit -> 'a) -> 'a |