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;

updated for release;