src/Pure/General/timing.ML
changeset 51507 ebd5366e7a42
parent 51228 dff3471dd8bc
child 51606 2843cc095a57
equal deleted inserted replaced
51505:9e91959a8cfc 51507:ebd5366e7a42