src/Pure/General/timing.ML
changeset 42135 da200fa2768c
parent 42042 264f8d0e899f
child 42819 cce39fdaad7b