src/Pure/Tools/ml_statistics.scala
Sun, 19 Mar 2017 11:56:56 +0100 wenzelm eliminated somewhat redundant inlined name (despite a7aa17a1f721);
Sun, 26 Feb 2017 22:13:07 +0100 wenzelm clarified defaults;
Sun, 26 Feb 2017 22:01:14 +0100 wenzelm tuned signature;
less more (0) -10 -3 tip