Tidied

merged

modernized and streamlined theory

provide somewhat incomplete naproche-20250125 for testing;

conservative update to stackage lts-22.15 and ghc-9.6.6;

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;

tuned names;

more direct emulation of HOL Light inferences: prefer Pure rules over HOL thms; represent hyps directly, using Thm.instantiate_frees followed by freeze' to ensure that no schematic vars remain (NB: Thm.generalize ignores type information); use Thm.implies_elim / Thm.elim_implies directly, with proper exceptions instead of implicitly remaining hyps that cause trouble later; def: proper freeze after retrieval of Isabelle thm;

tuned;

misc tuning: prefer specific variants of Thm.dest_comb;

more robust: explicit check for "Trueprop";

tuned;

more robust: explicit check for "Trueprop";

clarified signature: more uniform cterm operations, without context;

tuned;

tuned;

misc tuning: more antiquotations;

clarified exceptions;

tuned names, following HOL Light sources;

more robust alignments for HOL Light Release-3.0.0;

provide num_Axiom for HOL Light Release-3.0.0; tuned proofs;

tuned proofs;

more comments; more authors;

cleanup generated bounds;

discontinue special treatment of HOL Light CONJUNCTS: this is better done in Isabelle;

clarified bundle names, in terms of the "offline" tool; option to preserve raw proofs, to allow manual experimentation with "offline" and its "maps.lst";

proper result from "offline" tool;

optional maps.lst;

tuned output: proper progress;

support tracing (with proper guard); clarified signature: more explicit type name;

more README;

allow to load additional HOL Light files, after "hol.ml";

more complete bundle;