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.