src/Pure/General/timing.ML
changeset 55355 b5b64d9d1002
parent 51662 3391a493f39a
child 56333 38f1422ef473
equal deleted inserted replaced
55354:6ca9df01ac8c 55355:b5b64d9d1002