removed stuff moved to the Isabelle distribution

avoid java.net.URL, following Isabelle/a4118f530263;

merged

added lemma wf_on_iff_wf

changed number of consumed assumptions of wf_on_induct and wfp_on_induct

updated: standard Borel

use time_fun command

obsolete: base-line is macOS 11;

more robust: always assume x86_64 (or its emulation on ARM);

MLton lacks arm64-linux (see also 84f2d481d6d7);

more ambitious test "AFP (macOS 14 Sonoma, Apple Silicon)", as replacement for…

update to stack-2.15.3, stackage-lts-22.6, ghc-9.6.4;

tuned;

misc updates, tuning and clarification;

reformat source in jEdit (wrap margin 78);

merged

more accurate Markdown formatting, both for VSCode and Phabricator;

just one README.md;

merged

Splay tree analysis now uses time_fun command

tuned proofs to reduce verification time following Isabelle/7735645667f0

tuned

merged

support for etc/platform.props, to specify multi-platform directory structure…

more accurate platform directories: pkg/tool structure is hardwired in "go";

tuned;

clarified signature;

clarified modules;

clarified modules;

build Isabelle component for Go: all platforms;

misc tuning;

just one copy of darwin-universal.tar.gz;

documented running time function framework by Jonas Stahl

merge

feat(Transport) major improvement of overloaded properties + new relational…

feat(ML_Unification) add simplification+unification unifier; fix context merge…

fix(ML_Unification) replace binders before aeconv (avoids lowering)

merged

adapted to new definition of wf following Isabelle/033f90dc441d

merged

redefined wf as an abbreviation for "wf_on UNIV"

Two new lemmas by Eberl (requested by Paulson)

merged

adapted to isabelle/devel

merged

more uniform command names

tuned parameter order

shutdown lrzcloud2;

tuned NEWS

redefined wfP as an abbreviation for "wfp_on UNIV"

adapted to new definition of wfP following Isabelle/233d70cad0cf

updated url

merged

added lemma wellorder.wfp_on_less[simp]

merged

tuned proof

merged

suppress arm64-darwin, which does not support "-codegen native" (required for…

tuned signature: fewer warnings in IntelliJ IDEA;

update to sumatra_pdf-3.5.2;

update to jsoup-1.17.2;

enforce rebuild of Isabelle/ML;

proper bib entries (amending 82aaa0d8fc3b);

update to dotnet-8.0.203;

update to sqlite-3.45.2.0: clarified component name, following postgresql;

activate postgresql-42.7.3;

update to postgresql-42.7.3;

update to mlton-20210117-2, which covers x86_64-linux, x86_64-darwin, arm64…

isabelle update -u cite;

Patching some proofs, for of_nat_int_ceiling

raise error if benchmarking fails;

option for benchmark session;

add hosts option to run benchmark on the cluster from the command-line;

only start jobs early if they are due (cf. 1966578feff8);

Deletion of material that had been moved to the distribution

New material from a variety of sources (including AFP)

Multirelations_Heterogeneous: further results for convex-closure

build component for cvc5-latest (ef2bc3f735df);

merged

try proof method "order" in Sledgehammer's proof reconstruction

renamed lemma antisymp_on_reflcp to antisymp_on_reflclp

added Mirabelle action "order"

added lemma order_reflclp_if_transp_and_asymp

tuned proof

added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on

HOL-Library: added modulo/congruence for real numbers

remove laziness: no need, and errors during initialization loop with close();

only print schedule if relevant;

more general definition of meromorphicity; Weierstraß factorisation theorem

always provide build_database_server option in benchmark command;

always check if node is defined, e.g. for exists_next operation wit empty…

added some material about the Laurent expansion of zeta

fixed typo

disable taskset for now: performance impact is negative;

allow specifying initial schedule;

clarify use of num_threads vs. max_cpus;

clarified host: pre-load max threads;

clarified: more operations;

Remove stuff following Isabelle/d0205dde00bb and related changesets