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