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

merged

More tidying of old proofs

dropped redundant material (left-over from 5e3dd01a9eb2)

explicit check for (experimentally determined) border value

theory to rewrite arithmetic operations to bit shifts

merge

Compact notation for Suc numerals.

store the {l,g}fp-definition and the monotonicity theorem for inductive predicates (by Jan van Brügge)

make the definition of BNF bounds more easily accessible (by Jan van Brügge)

avoid theorem name clash (by Jan van Brügge)

introduce fewer constants in copy_bnf/lift_bnf (by Jan van Brügge)

Some work on an ancient theory file. And a weird failure in Float.thy

simplified old proofs

polished messy proofs

moved lemmas to book

merged

tuned messages: more verbosity;

more explicit default_port;

tuned messages;

tuned;

proper initialization of settings: avoid accidental intrusion from parent process environment;

clarified solr_data directory, provided via settings;

explicit settings FIND_FACTS_WEB and option -w, outside of source (immutable) directory;

tuned message;

implicit session build, similar to "isabelle export";

tuned message;

proper Console_Progress as for other command-line tools;

tuned messages: more formal;

clarified signature: progress is usually optional;

clarified names: "peek" usually refers to evolving mutable state;

more to check;

tuned: avoid "open" in ML and "import _" in Scala;

tuned messages;

tuned headers;

more to check;

clarified names;

clarified signature and modules;

tuned;

avoid conflict with slf4j from sqlite (see also dcddfe4f43a3), notably this message on "isabelle find_facts": SLF4J(W): Class path contains multiple SLF4J providers. SLF4J(W): Found provider [org.slf4j.nop.NOPServiceProvider@1576514a] SLF4J(W): Found provider [org.apache.logging.slf4j.SLF4JServiceProvider@6a84d4e3] SLF4J(W): See https://www.slf4j.org/codes.html#multiple_bindings for an explanation. SLF4J(I): Actual provider is of type [org.slf4j.nop.NOPServiceProvider@1576514a]

misc tuning;

tuned: fewer warnings in IntelliJ IDEA;

tuned headers;

tuned headers;

more NEWS + CONTRIBUTORS;

tuned comments;

tool wrappers with specific java options, notably classpath "$SOLR_JARS";

clarified options;

proper component src/Tools/Find_Facts; clarified directory structure;

components for find_facts;

suppress duplicate slf4j-api --- already provided by sqlite;

clarified solr settings; proper version;

proper platform.exe;

activate admin tools; clarified elm settings;

original sources of find-facts 271b5af0c4c8;

Simplified a lot of messy proofs

compatibility with Scala 3

more correct code generation for string literals

made lemma visible

fixed a typo

Correction to pretty printing for set intervals, allowing a line break if necessary for a large expression

tuned documentation and order of instantiated facts

merged

update cygwin near 3.5.5-1, see also https://cygwin.com/pipermail/cygwin-announce/2024-December/012023.html

direct symbolic implementations of and, or, xor on integer

corrected

merged

remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);

rebuild cvc5 component (still inactive); more robust workaround on all platforms, avoid crash of "sledgehammer [cvc5]" seen on x86_64-linux after line 75 of "$AFP/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy";

tuned spacing

merged

tuned Sledgehammer caching

Rename "suggest_of" to "instantiate"

merged

added lemmas

discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);

more markup, notaly for LaTeX output: treat record fields as quasi-consts;

tuned: more direct string comparison (see also 6e25f82056ad, where the explanation was actually wrong: about fast_string_ord instead of string_ord);

update release name;

Added tag Isabelle2025-RC0 for changeset bcb793b951c0

proper NEWS section;

proper latin "A" instead of greek "Alpha";

update to current jcef-1.0.61;

recovered "isabelle component_jcef" from bf537a75e872, adapted to 9fe5d8c70352 and 2a99fcb283ee;

tuned proofs;

tuned proofs;

more robust afp_repository, with regular hgweb URLs;

more documentation;

merged

tuned;