more operations;

clarified signature: init_state vs. init_unsynchronized;

more thorough "isabelle build_process -C -r -f";

more operations;

tuned signature;

tuned signature: more uniform SQL.Data instances;

tuned signature;

tuned signature;

disable write_updates from f425bbc4b2eb for now: "isabelle build_process -rf" does not quite work yet;

revert part of 5969ead9f900 that does not quite work yet: only one accidental host is used;

record updates within database, based on serial;

proper tables (amending 4611b7b47b42);

tuned;

clarified signature: improved data integrity;

clarified modules;

clarified modules;

obsolete;

misc tuning: prefer Build_Process.Update operations;

misc tuning and clarification: prefer explicit type Build_Process.Update;

misc tuning and clarification;

tuned signature;

clarified data representation: more uniform treatment of State.Pending vs. State.Running;

tuned: drop pointless SQL.order_by (see also 5f706f7c624b);

upgrade pretty_maybe_quote following 2746dfc9ceae;

tuned;

eliminate odd aliases (see also 2746dfc9ceae);

tuned signature: prefer bottom-up construction;

tuned;

tuned signature;

clarified signature;

tuned;

more operations for Build_Log.Meta_Info: prefer explicit types;

more operations for Date and Time;

more accurate patterns --- reverting unused fc3ba0a1c82f;

remove unused/fragile option (amending db37cae970a6) --- universal_table requires pull_date tables;

prefer explicit option "build_log_verbose";

tuned whitespace;

additional build_log column "session_start", with implicit upgrade of database schema;

more robust build_start for master and workers (via database);

more accurate progress.now(), notably for Database_Progress;

update NEWS;

activate E 3.0 after testing by Martin Desharnais, see also db72d9920186 and 788f11af9822;

merged

added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]

parallelize schedule optimization;

revised NEWS: OCaml / OPAM appears to be fine on arm64-linux, e.g. Ubuntu 22.04;

update to current long-term-support version dotnet-8.0.x;

merged

proper release bundle_name (amending 0e7dd3eaa6e8);

more multiset lemmas

optional cartouche syntax and proper name printing in atp Isar output

merged

removed unused variable

added virtual, greedy portfolio for E 3.0

tuned;

tuned signature;

Added tag Isabelle2024-RC0 for changeset 98f009f56400

updated for release;

updated for release;

clarified signature;

misc tuning for release;

tuned whitespace: avoid TABs;

avoid suspicious Unicode;

tuned whitespace;

tuned signature: fewer warnings in IntelliJ IDEA;

merged

update NEWS;

update cygwin near 3.5.1-1, also see https://cygwin.com/pipermail/cygwin-announce/2024-February/011524.html and https://cygwin.com/pipermail/cygwin-announce/2024-February/011611.html

drop unused Task.info field;

proper guard_time (amending 752806151432);

proper dynamic access (amending c3f07c950116);

more robust, notably for remote process (via SSH);

prefer dynamic objects, following a5fda30edae2;

proper dynamic access (amending 52b5c7c8e6d9);

clarified signature: incorporate guard into Logger;

merged

added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp

Moving valuable library material from Martingales into the distribution

clarified signature; sleep unconditionally: avoid aggressive database access;

clarified module signature and state;

tuned messages;

omit somewhat pointless message, following b7187d4cdf68;

more robust handling of uninitialized value, notably Build_Process.progress;

tuned

partially revert f1f08ca40d96: benchmark data needs to be present before timing data is loaded;

clarified module signature and state;

tuned signature: more protected operations;

database performance tuning: just one synchronized_database for main loop body;

tuned;

more robust: assume that database is exclusive for this Progress instance --- always close on exit (see also bf377e10ff3b);

more robust: imitate Isabelle/ML operation more closely (after 26a43785590b); logical_cores is e.g. relevant for server-arm.sketis.net, where /proc/cpuinfo looks quite different;

tuned;

tuned proof: avoid z3 to make it work on arm64-linux;

official support for arm64-linux, despite a few missing tools;

discontinue unstable z3-4.4.1 for arm64-linux from Debian (in contrast to 796ae338eb9d and 87718883c8b9);

proper platform_name/platform_dir for native arm64-darwin: already published in 788f11af9822 after manual adjustment;

update to scala-3.3.3; enforce rebuild of Isabelle/Scala + Isabelle/ML;

provide e-3.0.03 on all platforms, including arm64-linux and arm64-darwin --- still inactive;

update NEWS, following 0d7c7fe65638;

provide cvc5-1.1.1 for testing --- still inactive;

rebuild bash_process executables on current reference platforms, including native arm64-darwin; enforce rebuild of Isabelle/Scala + Isabelle/ML;

tuned NEWS, see also c62003e05e46;

update NEWS, following ea1913c953ef;

tuned whitespace according to jEdit mode parameters ":wrap=hard:maxLineLen=72:";

more explicit NEWS (see 3648e9c88d0c);

NEWS for a53287d9add3, 3e30ca77ccfe;

add option for unify trace (now disabled by default as printing is excessive and rarely used);

tuned unify trace option names;

more scalable: avoid potentially expensive ordering of underlying key data type, e.g. in MESON.Cache of Naproche;

updated to stack-2.15.1, lts-22.6, ghc-9.6.3;

merged

tuned name

new simplifier trace_op for tracing simproc calls

merged

Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers

support Zipperposition's skolemization in generated Isar proofs

improved output in simps_case_conv;

improved output in inductive module;

simplifier: no trace info from simprocs unless simp_debug = true.

deal with new-style Vampire skolemization in reconstructed Isar proofs