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;