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;