nat_diff_split lemmas

NEWS

tuned whitespace

added lemmas ex_terminating_rtranclp_strong and ex_terminating_rtranclp

added lemma strict_partial_order_wfp_on_finite_set

proper order of operations: archive before purge;

more robust (see also 9601f5582f33);

tuned spelling;

clarified NEWS: not user-relevant;

tuned documentation;

clarified default of flatlaf.useNativeLibrary=false, for cross-platform GUI uniformity;

just one flatlaf version: native libraries are optional;

tuned;

merged

clarified name;

documentation about Build_Manager;

tuned;

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;