src/Pure/General/timing.ML
changeset 42405 13ecdb3057d8
parent 42042 264f8d0e899f
child 42819 cce39fdaad7b