src/Pure/General/timing.ML
changeset 49082 d71cdd1171c3
parent 44440 aa2abd81f460
child 50777 20126dd9772c
equal deleted inserted replaced
49081:092668a120cc 49082:d71cdd1171c3