Distinguish two versions of cvc5 -- one used for Sledgehammer, one for proof reconstruction in SMT. provided by Mathias Fleury

tuned whitespace;

prefer static object, while class is required for "services" (see 47eb96592aa2);

clarified directories; clarified names;

tuned signature;

tuned: prefer explicit update operation for immutable options;

tuned message;

more robust type, with explicit default;

tuned usage message;

clarified signature;

more robust defaults;

merged

added lemmas relpow_trans[trans] and relpowp_trans[trans]

more on disjunctive addition/subtraction

merged

prefer physical processors (see also 4b014e6c1dfe and 26a43785590b);

more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");

more robust default;

more accurate, notably on lxbroy10 and vmnipkow9;

clarified num_processors: follow Poly/ML (with its inaccuracies);

clarified modules, following Isabelle/ML;

clarified signature;

tuned comments;

merged

the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses

merged

A few lemmas brought in from AFP entries

merged

made destructor-view tactic more robust (by Jan van Brügge)

performance optimization;

clarified names;

clarified scheduler: proper split into scheduler, generator, and priority rules (following 32d00ec387f4);

proper "linux_arm", amending 76ad72736e9e;

more lemmas

new lemmas involving Ramsey numbers, infinite sets

simplified class specification

Removal of duplicate code

Two new theorems

more lemmas and more correct lemma names

NEWS: corrected the definition of convexity of functions

Further lemmas concerning complexity and measures

Correct the definition of a convex function, and updated the proofs

merged;

update to windows_app-20240205, with executables for linux, linux_arm, macos;

omit redundant options;

tuned README;

uniform build of binutils for linux, linux_arm, macos;

fix reconstruction of Alethe's and_pos rule

added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult

proper target option, following package binutils-mingw-w64-x86-64 from Debian/Ubuntu;

updated windows_app based on launch4j-3.50-linux-x64, without rebuilding GNU binutils (missing COFF target pe-i386);

proper sfx_archive_name;

clarified options;

more robust;

build Isabelle windows_app component from GNU binutils and launch4j;

proper windows_app/launch4j-linux_arm;

merged

A small number of new lemmas

explicit reference to code_dt

made lift_bnf more robust for abstract types with 'phantom' type variables

rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory "HOL-ex.BigO"; uniform baseline for "linux" and "linux_arm";

proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb);

proper bash syntax (amending 0631dfc0db07);

tuned proof: avoid z3;

tuned proof: avoid z3 to make it work on arm64-linux;

tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux;

merged

more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);

strengthened class parity

proper accessible paths for web server;

more informative message (amending b8a6b2ec85a2);

merged

more robust: do not affect "$ISABELLE_HOME_USER/contrib" on master node;

avoid excessive ML heap on this 16GB node;

more robust (amending c9774306a879);

proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;

clarified symbolic host name;

allow remote_build on this host (server-arm), without conflicts of this "isabelle_self";

more robust message;

A few more new theorems taken from AFP entries

merged

define_time_function: avoid unused let's

common type class for trivial properties on div/mod

more robust (amending 1600fb749c54), to support the following corner case: schematic_goal "PROP ((?f :: ?'a \<Rightarrow> _) (x :: ?'a))" apply (tactic \<open>PRIMITIVE (Thm.instantiate (TVars.make1 ((("'a", 0), []), @{ctyp prop}), Vars.empty))\<close>) oops

proper test options;

proper history_base for linux_arm;

updated to PostgreSQL 12 on Ubuntu 20.04; more accurate command-line;

routine build + test for linux_arm;

disable test on "augsburg1": machine will be dismantled;

add approximation factors in build schedule to estimate build times more conservatively;

merged

Type class patch suggested by Achim Brucker, plus tidied lemma

rearranged and reformulated abstract classes for bit structures and operations

Three new lemmas

tuned proof: avoid z3 to make it work on arm64-linux;

update to jdk-21.0.2; enforce rebuild of Isabelle/Scala + Isabelle/ML;

make build process state protected to avoid copying in subclasses (e.g. for database connections);

add build_sync tag to sync certain options (e.g., build_engine) across build processes;

clarified Mercurial version: presumably the last version that supports both python2 and python3;

more robust: avoid crash on non-Linux systems;

clarified webserver names;

proper Apache.php_name;

proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);

tuned source structure;

more robust systemd configuration;

more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";

tuned whitespace in generated file;

tuned;

clarified modules;

recover Url.is_wellformed from before d8330439823a, e.g. relevant for JEdit_Resources.read_file_content (the URI alone does not necessarily have a protocol prefix, so plain file-path would be treated as URL);

proper php-fpm configuration for nginx;

support multiple webservers: Apache or Nginx;

tuned;

clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);

unused;

enforce rebuild of Isabelle/Scala + Isabelle/ML;

updated to postgresql-42.7.1;

updated to sqlite-jdbc-3.45.0.0, including slf4j-1.7.36;

update to llncs-2.23; update src/Doc/Demo_LLNCS to include the new mandatory section "Disclosure of Interests";

clarified bootstrap;