use ssh host for default address;

tuned;

clarified option name;

clarified options: extra ssh connection to cluster of build_manager;

tuned output;

tuned: more standard;

merged;

more NEWS;

updated to flatlaf-3.5.4, with fallback on 2.6 for arm64-linux;

update naproche-20250201: rebuilt executables (just one copy), provide most PDFs;

tuned whitespace;

documentation about Find_Facts;

more standard: let OS pick random port by default;

clarified platforms; update to hugo-0.142.0;

tuned NEWS;

merged

more canonical formatting

add hook to insert premises in the order solver

less NEWS (see also afae60d6ff15);

switch from CVC5 to cvc5, including updates of internal tool references;

more robust wrt. Par_List.map in Browser_Info.build(), see also 2fff9ce6b460 and 787a203a20b6;

more thorough cleanup;

more options for build_release: support bundled browser_info and Find_Facts database;

more standard directory structure;

tuned output;

suppress MacOS.jar from jEdit 5.7.0, following 65fd0f032a75;

tuned GUI: attempt to improve divider mobility;

rebuild jedit component;

make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;

more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');

more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);

clarifed terminology

extracted the ^^ subtheory for modularity reasons

tuned

merged

tuned;

minor performance tuning;

tuned;

tuned names;

minor performance tuning: avoid somewhat indirect filter / add_consts;

clarified signature: more standard map_data;

misc tuning;

clarified signature with minor performance tuning: avoid Context.proof_of with its Proof_Context.init_global;

tuned names;

more explicit tests for non-PolyML SML platforms

typo

merged

more NEWS;

clarified syntax;

support for "no" polarity of 'adhoc_overloading' vs. 'no_adhoc_overloading';

more operations;

clarified signature: proper ML interface to main command, without exposing too many internals;

tuned signature: more explicit Type.raw_equiv;

more liberal type equivalence, following thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy from AFP/e69d71bc07c4;

move theory "HOL-Library.Adhoc_Overloading" to Pure;

discontinue odd "-build" suffix altogether (see also f51b0b54b20b, bec95e287d26, 6b45a1568637);

more frugal exports

clarified scopes

more correct SML for SML/NJ

more explicit real operations

merged

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";