clarified signature;

tuned;

unused (see also ea35afdb1366);

more robust transaction_lock: avoid overlapping data spaces; clarified modules;

merged

The sym_diff operator (symmetric difference)

disable lxbroy10 for now: technical problems with cooling;

A couple of new lemmas involving cardinality

merged

tuned;

more robust;

proper build_progress for local messages;

proper SQL query;

Another tranche of HOL Light material on metric and topological spaces

merged

EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis

merged

more robust "stop": further "stamp" ticks may happen afterwards;

removed junk;

tuned signature;

tuned: prefer Scala over Java;

clarified signature;

tuned;

more SQL data;

add proof method "order" to command "try0"

tuned signature;

clarified static Build_Process.Context vs. dynamic Build_Process.State; more dynamic Build_Process.Sessions, to accomodate multiple workers (and multiple builds);

tuned signature: more operations;

clarified signature: proper equals/hashCode;

more robust database setup;

clarified signature;

clarified signature;

New theory Leftist_Heap_List

added [simp]

merged

proper build_master.build_uuid;

proper session_init *after* deleting db files (amending af6c493b0441);

clarified signature: more concise data;

tuned output;

more robust;

clarified signature: better default;

show only active builds;

clarified output;

tuned;

support for identified builds; more complete implementation of "isabelle build_worker";

clarified signature: more operations and options;

tuned;

clarified signature;

clarified signature;

more robust close() after failed initialization;

avoid repeated open_database_server: synchronized transaction_lock;

tuned signature;

more robust: proper transaction_lock;

tuned signature;

tuned signature;

tuned signature;

clarified signature: more options;

tuned;

clarified database for heaps: do not depend on build_database_test;

clarified signature;

tuned signature;

More metric space material

merged

New and generalised analysis lemmas

tuned names

clarified signature: prefer explicit combinator;

unused;

restore heaps from database, which takes precedence over file-system;

tuned;

more operations;

tuned;

more robust try-finally;

tuned signature;

proper clean_entry;

afford larger build_database_slice for better compression (HOL: 1 slice, HOL-Proofs: multiple slices for testing);

prefer system option;

clarified signature: more explicit class SQL.Data;

proper ML_Heap.clean_entry;

tuned signature;

tuned;

store heaps within database server;

tuned signature;

clarified modules;

tuned signature;

clarified modules;

clarified modules;

early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;

merged

proper close;

separate host.db for independent db.transaction_lock;

tuned comments;

omit redundant data: already stored in progress database;

tuned signature: more operations;

proper support for SQLite: avoid conflicts on transaction_lock;

minor performance tuning: avoid external process;

clarified signature;

obsolete;

tuned;

tuned signature;

tuned signature;

clarified signature;

tuned;

clarified signature;

tuned;

proper pattern (amending da5cc332ded3);

tuned signature;

proper hostname from build_context;

prefer Database_Progress, which is more robust (amending afb1a19307c4);

support for Database_Progress;

tuned signature: more operations;

tuned signature: more operations;

tuned signature: more operations;

clarified signature;

optional description in Eisbach "method" command;

disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice

Added tag Isabelle2023-RC0 for changeset f4221ae7544c

updated to zstd-jni-1.5.5-4;

updated to postgresql-42.6.0;

back to more concise build_release, thanks to build_host_macos = "mini3";

more PLATFORMS;