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;

tuned README;

proper settings;