build cluster host specifications are based on registry entries (table prefix "host");

more robust init;

clarified signature: more operations;

support interpreted/typed entries via Registry.Category and Registry.Table;

clarified signature: more operations;

clarified output;

support for global registry;

clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";

slightly less technical formulation of very specific type class

weakened dependency

explicit type class for discrete linordered semidoms

proper dummy timing entries;

use only finished sessions in timing data;

tuned;

performance tuning for build schedule: explicit schedule generation, without mixing heuristics;

performance tuning for build schedule: faster stopping;

performance tuning for timing heuristic: pre-calculate graph operations;

move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);

clarified signature: emphasize mutable instance;

clarified signature: more operations;

support for explicit SSH hostname;

proper local host (amending 62d7ef1da441);

merged

added lemma

proper default for disjunction (amending 9f7a94117666);

tuned;

more operations;

avoid option -C: free this latter for build-related configuration;

more direct indentation, using Symbol.spaces;

clarified signature;

more accurate treatment of surrounding whitespace;

obsolete (see also f627ab8c276c);

tuned signature;

clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;

clarified modules;

tuned signature;

tuned;

proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d);

more tests;

clarified exploration of history: more uniform options;

tuned;

tuned;

enable multi-builds (again, see also 0c7419d3dd59);

explore history more thoroughly;

tuned signature;

clarified "recent" time: days <= 0 means infinity (no constraint);

tuned whitespace;

proper exploration of older history: avoid premature fallback on current "rev" (see also d3d5cb2d6866, 6706d6f0afda);

clarified signature;

tuned output;

tuned;

tuned message;

proper option;

merged

proper SQL.string syntax, following actual SQL standard instead of historic variations before PostgreSQL 9.1; ensure connection defaults required for string literals;

Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family

merged

prefer Time.scale(), following Isabelle/ML;

proper benchmark command;

merged

proper progress (see also 45d570945fe4);

improved build messages;

clarified;

merged