src/Pure/General/timing.ML
changeset 54715 a13aa1cac0e8
parent 51662 3391a493f39a
child 56333 38f1422ef473
equal deleted inserted replaced
54714:ae01c51eadff 54715:a13aa1cac0e8