Sat, 11 Nov 2023 16:01:57 +0100 clarified output;
wenzelm [Sat, 11 Nov 2023 16:01:57 +0100] rev 78940
clarified output;
Sat, 11 Nov 2023 13:31:14 +0100 support for global registry;
wenzelm [Sat, 11 Nov 2023 13:31:14 +0100] rev 78939
support for global registry;
Fri, 10 Nov 2023 16:03:52 +0100 clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";
wenzelm [Fri, 10 Nov 2023 16:03:52 +0100] rev 78938
clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";
Thu, 09 Nov 2023 15:11:52 +0000 slightly less technical formulation of very specific type class
haftmann [Thu, 09 Nov 2023 15:11:52 +0000] rev 78937
slightly less technical formulation of very specific type class
Thu, 09 Nov 2023 15:11:51 +0000 weakened dependency
haftmann [Thu, 09 Nov 2023 15:11:51 +0000] rev 78936
weakened dependency
Thu, 09 Nov 2023 15:11:51 +0000 explicit type class for discrete linordered semidoms
haftmann [Thu, 09 Nov 2023 15:11:51 +0000] rev 78935
explicit type class for discrete linordered semidoms
Thu, 09 Nov 2023 19:06:50 +0100 proper dummy timing entries;
Fabian Huch <huch@in.tum.de> [Thu, 09 Nov 2023 19:06:50 +0100] rev 78934
proper dummy timing entries;
Thu, 09 Nov 2023 17:58:21 +0100 use only finished sessions in timing data;
Fabian Huch <huch@in.tum.de> [Thu, 09 Nov 2023 17:58:21 +0100] rev 78933
use only finished sessions in timing data;
Thu, 09 Nov 2023 16:39:36 +0100 tuned;
Fabian Huch <huch@in.tum.de> [Thu, 09 Nov 2023 16:39:36 +0100] rev 78932
tuned;
Thu, 09 Nov 2023 15:45:51 +0100 performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de> [Thu, 09 Nov 2023 15:45:51 +0100] rev 78931
performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Thu, 09 Nov 2023 11:49:08 +0100 performance tuning for build schedule: faster stopping;
Fabian Huch <huch@in.tum.de> [Thu, 09 Nov 2023 11:49:08 +0100] rev 78930
performance tuning for build schedule: faster stopping;
Thu, 09 Nov 2023 11:41:19 +0100 performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de> [Thu, 09 Nov 2023 11:41:19 +0100] rev 78929
performance tuning for timing heuristic: pre-calculate graph operations;
Wed, 08 Nov 2023 11:08:03 +0100 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de> [Wed, 08 Nov 2023 11:08:03 +0100] rev 78928
move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Thu, 09 Nov 2023 14:28:17 +0100 clarified signature: emphasize mutable instance;
wenzelm [Thu, 09 Nov 2023 14:28:17 +0100] rev 78927
clarified signature: emphasize mutable instance;
Thu, 09 Nov 2023 14:22:19 +0100 clarified signature: more operations;
wenzelm [Thu, 09 Nov 2023 14:22:19 +0100] rev 78926
clarified signature: more operations;
Thu, 09 Nov 2023 13:31:09 +0100 support for explicit SSH hostname;
wenzelm [Thu, 09 Nov 2023 13:31:09 +0100] rev 78925
support for explicit SSH hostname;
Thu, 09 Nov 2023 11:30:33 +0100 proper local host (amending 62d7ef1da441);
wenzelm [Thu, 09 Nov 2023 11:30:33 +0100] rev 78924
proper local host (amending 62d7ef1da441);
Wed, 08 Nov 2023 21:45:02 +0100 merged
nipkow [Wed, 08 Nov 2023 21:45:02 +0100] rev 78923
merged
Wed, 08 Nov 2023 21:44:44 +0100 added lemma
nipkow [Wed, 08 Nov 2023 21:44:44 +0100] rev 78922
added lemma
Wed, 08 Nov 2023 20:31:29 +0100 proper default for disjunction (amending 9f7a94117666);
wenzelm [Wed, 08 Nov 2023 20:31:29 +0100] rev 78921
proper default for disjunction (amending 9f7a94117666);
Wed, 08 Nov 2023 19:04:44 +0100 tuned;
wenzelm [Wed, 08 Nov 2023 19:04:44 +0100] rev 78920
tuned;
Wed, 08 Nov 2023 16:05:22 +0100 more operations;
wenzelm [Wed, 08 Nov 2023 16:05:22 +0100] rev 78919
more operations;
Wed, 08 Nov 2023 15:37:15 +0100 avoid option -C: free this latter for build-related configuration;
wenzelm [Wed, 08 Nov 2023 15:37:15 +0100] rev 78918
avoid option -C: free this latter for build-related configuration;
Wed, 08 Nov 2023 15:10:19 +0100 more direct indentation, using Symbol.spaces;
wenzelm [Wed, 08 Nov 2023 15:10:19 +0100] rev 78917
more direct indentation, using Symbol.spaces;
Wed, 08 Nov 2023 13:14:59 +0100 clarified signature;
wenzelm [Wed, 08 Nov 2023 13:14:59 +0100] rev 78916
clarified signature;
Wed, 08 Nov 2023 13:00:24 +0100 more accurate treatment of surrounding whitespace;
wenzelm [Wed, 08 Nov 2023 13:00:24 +0100] rev 78915
more accurate treatment of surrounding whitespace;
Wed, 08 Nov 2023 12:41:41 +0100 obsolete (see also f627ab8c276c);
wenzelm [Wed, 08 Nov 2023 12:41:41 +0100] rev 78914
obsolete (see also f627ab8c276c);
Wed, 08 Nov 2023 12:00:29 +0100 tuned signature;
wenzelm [Wed, 08 Nov 2023 12:00:29 +0100] rev 78913
tuned signature;
Wed, 08 Nov 2023 11:53:38 +0100 clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
wenzelm [Wed, 08 Nov 2023 11:53:38 +0100] rev 78912
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
Tue, 07 Nov 2023 15:59:02 +0100 clarified modules;
wenzelm [Tue, 07 Nov 2023 15:59:02 +0100] rev 78911
clarified modules;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip