unused;

prefer scalable Bytes.T;

missing recursive let-expansion in SMT translation

merged

added lemma monotone_on_o

redefined mono_on and strict_mono_on as an abbreviation of monotone_on

changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates

more robust CSV syntax, e.g. for "pull_date";

merged

more scalable generated files and code export, using Bytes.T;

more operations;

proper execution of Bytes.write; tuned;

Avoid calculations where not necessary.

Prefer existing horner sum combinator.

Executable lexords.

Less warnings.

merged

more operations;

removed unused operations; tuned (again);

clarified signature: more operations;

tuned;

tuned comments;

tuned;

clarified session resources for bootstrap, notably for Scala functions;

tuned;

clarified signature;

tuned signature;

clarified types and defaults;

merged

added lemmas monotone{,_on}_multp_multp_image_mset

added lemmas monotone_on_empty[simp] and monotone_on_subset

added predicate monotone_on and redefined monotone to be an abbreviation.

merged

NEWS;

support XZ compression in Isabelle/ML;

prefer scalable byte strings;

more scalable byte messages, notably for Scala functions in ML;

tuned comments;

clarified ML pretty printing;

clarified signature: more operations;

tuned signature;

tuned comments;

tuned signature: more operations;

tuned signature: more operations;

tuned signature;

clarified signature: avoid repeated string copying via Substring.slice;

support for scalable byte strings, with incremental construction;

clarified signature;