src/Pure/ML/ml_statistics.scala
Sat, 01 Jun 2024 12:31:06 +0200 wenzelm clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
Sun, 26 Mar 2023 12:53:53 +0200 wenzelm clarified signature: more explicit types;
Sun, 26 Mar 2023 12:41:34 +0200 wenzelm clarified signature: more explicit types;
Fri, 24 Feb 2023 20:40:50 +0100 wenzelm tuned;
Mon, 06 Feb 2023 16:29:19 +0100 wenzelm tuned signature;
Sat, 28 Jan 2023 16:08:43 +0100 wenzelm clarified signature: more explicit types;
Sat, 28 Jan 2023 15:38:36 +0100 wenzelm tuned;
Sat, 28 Jan 2023 15:35:43 +0100 wenzelm clarified signature: more robust field_scale;
Sat, 28 Jan 2023 15:04:15 +0100 wenzelm clarified signature: more explicit types;
Fri, 27 Jan 2023 18:59:48 +0100 wenzelm tuned;
Thu, 21 Apr 2022 10:03:38 +0200 wenzelm tuned signature;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Thu, 31 Mar 2022 21:51:19 +0200 wenzelm tuned: avoid problems with scala3;
Sat, 27 Nov 2021 14:03:44 +0100 wenzelm tuned output;
Sat, 27 Nov 2021 13:55:03 +0100 wenzelm tuned;
Mon, 17 May 2021 14:54:03 +0200 wenzelm more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases;
Sun, 25 Apr 2021 22:33:15 +0200 wenzelm avoid "exec" to change the winpid;
Wed, 31 Mar 2021 22:10:56 +0200 wenzelm tuned signature -- more explicit types;
Thu, 04 Mar 2021 21:04:27 +0100 wenzelm clarified signature --- fewer warnings;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Sun, 10 Jan 2021 13:04:29 +0100 wenzelm more informative errors: simplify diagnosis of spurious failures reported by users;
Sat, 02 Jan 2021 22:22:34 +0100 wenzelm clarified signature: absorb XZ.Cache into XML.Cache;
Thu, 10 Sep 2020 21:14:50 +0200 wenzelm clarified modules;
Fri, 28 Aug 2020 16:14:19 +0200 wenzelm more robust interpretation of data;
Thu, 27 Aug 2020 12:43:06 +0200 wenzelm tuned;
Thu, 27 Aug 2020 12:34:10 +0200 wenzelm clarified signature;
Sat, 15 Aug 2020 13:45:25 +0200 wenzelm clarified names;
Thu, 13 Aug 2020 15:11:30 +0200 wenzelm support JVM runtime statistics;
Thu, 13 Aug 2020 12:38:44 +0200 wenzelm clarified order for GUI;
less more (0) -50 -30 tip