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

database performance tuning: prefer light-weight IPC over heavy-duty transactions;

tuned signature; tuned output;

tuned signature: follow PostgreSQL syntax instead of JDBC API;

more robust shutdown: interruptible database connection;

clarified signature: more convenient send/receive operations;

clarified versions for documentation;

merged

clarified signature: avoid hardwired values;

clarified IPC via database server: receive notifications quasi-spontaneously via auxiliary thread;

minor performance tuning: just 1 transaction for slices <= 1;

tuned;

tuned whitespace;

tuned signature;

clarified signature: fewer warnings in IntelliJ IDEA;

removed unused database_server (amending 32ca3d1283de);

timing function generation bug fix by Jonas Stahl

tuned signature: more types, fewer warnings in IntelliJ IDEA;

new less ad hoc implementation of the 'moura' tactic for skolemization

more thorough Store.clean_output (amending 1fa1b32b0379);

clarified signature: Build_Process tells how to clean sessions;

clarified signature;

tuned;

tuned;

minor performance tuning;

tuned;

tuned signature;

tuned, following 7a1153c95bf9;

merged

tuned signature: fewer warnings in IntelliJ IDEA;

proper usage;

recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;

clarified signature;

more robust: make double-sure that heap digest is present;