tuned;

tuned;

clarified pattern matching;

misc tuning;

misc tuning and clarification;

tuned;

clarified exceptions and messages: use "error" only for user-errors, not system failures;

minor performance tuning: more elementary operations;

minor performance tuning;

clarified inst_type: more direct Thm.instantiate_frees;

more direct Thm.free: avoid re-certification;

clarified signature: more explicit types;

tuned names;

tuned names;

tuned signature;

tuned;

tuned signature;

clarified signature: more standard Isabelle/ML;

clarified signature;

more robust import_file path: proper master_directory; support for compressed proofs.zst (e.g. via "zstd -8");

tuned signature: more operations;

unused;

tuned signature, following Isabelle/Scala;

clarified signature, following Isabelle/Scala;

clarified pattern via antiquotations;

misc tuning and clarification;

tuned;

clarified make_type: proper make_name;

tuned;

tuned;

clarified signature: more standard Isabelle/ML;

reproducible construction of HOL Light export bundle;

tuned messages;

more robust options; more robust lines;

clarified signature: more explicit operations;

tuned;

tuned: prefer inlined thms;

tuned proofs;

proper GUI.Style_HTML.make_text, e.g. for term "x < y";

clarified signature: more explicit operations;

provide less ambitious "isabelle ocaml_setup_base", notably for platforms without gmp-dev;

clarified signature: more explicit operations;

update to ocaml-base-compiler.4.14.1, which coincides with ocaml on Ubuntu 24.04;

isabelle_id: report sync id, if available;

clarified: sync_id operation, similar to archive_id;

build schedule: limit history length;

tuned whitespace;

restrict check to PolyML