conservative update to stack-2.15.7;

merged

merged

Tidying more old proofs

discontinue old Java 17 LTS;

update versions for release -- one behind current jedit-5.7.0;

more explicit system dependencies;

proper executable from "isabelle ocaml_opam env";

update to postgresql-42.7.5; update to sqlite-3.48.0.0; enforce rebuild of Isabelle/ML and Isabelle/Scala;

update to jdk-21.0.6; enforce rebuild of Isabelle/ML and Isabelle/Scala;

update for release;

misc tuning for release;

more NEWS;

more authors;

merged

tuned names: follow HOL Light; tuned signature: no proactive export of internal operations;

more antiquotations;

support for @{instantiate (no_beta) ...};

minor performance tuning: more fine-grained guard to skip irrelevant items;

proper treatment of variables with the same name, but different sorts/types: this routinely happens in HOL Light (see also 0e2f019477e2), as well as theory "HOL-Algebra.Algebraic_Closure_Type" (line 77);

tuned output;

minor performance tuning: omit redundant inst_cterm;

tuned signature: more operations;

misc tuning: more concise operations on prems (without change of exceptions); discontinue odd clone Drule.cprems_of (see also 991a3feaf270);

tuned: prefer Thm.prem_of, which differes wrt. exceptions that are not handled here;

tuned signature: more explicit operations;

tuned: more direct Thm.cprem_of;

misc tuning;