changeset 62945 | c38c08889aa9 |
parent 62459 | 7a5d88dd8cc9 |
child 63806 | c54a53ef1873 |
--- a/src/Pure/ML/ml_statistics.ML Sun Apr 10 21:46:12 2016 +0200 +++ b/src/Pure/ML/ml_statistics.ML Sun Apr 10 22:27:05 2016 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/ML/ml_statistics.ML Author: Makarius -ML runtime statistics for Poly/ML 5.5.0 or later. +ML runtime statistics. *) signature ML_STATISTICS =