tuned signature;

tuned, following 7a1153c95bf9;

merged

tuned signature: fewer warnings in IntelliJ IDEA;

proper usage;

recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;

clarified signature;

more robust: make double-sure that heap digest is present;

tuned;

minor performance tuning: just one transaction for log_db without heap;

tuned;

proper store.cache.compress;

tuned whitespace;

clarified store_session: heap requires process_result.ok, but log_db is always stored; clarified ML_Heap.clean_entry vs. ML_Heap.init_entry;

unused;

tuned;

tuned names;

tuned names;

clarified database layout;

tuned signature; tuned messages;

clarified signature;

more accurate types;

build local log_db, with store/restore via optional database server; tuned messages;

propagate property "isabelle.debug", notably for Java/Scala exception trace;

tuned;

proper treatment of "isabelle build_process -C" (amending 0cac7e3634d0);

clarified signature; more robust slice_size;

clarified names;

more explicit build_cluster flag to guard open_build_database server;

tuned;

clarified signature;

simplified specification of type class semiring_bits

New material about transcendental functions, polynomials, et cetera, thanks to Manuel Eberl

merged

A small collection of new and useful facts, including the AM-GM inequality

remove selected occurrences of 'moura' tactic

added lemmas relpowp_left_unique and relpow_left_unique

added lemmas relpowp_right_unique and relpow_right_unique

use define_time_fun

time funs: +1 instead of 1+

minor performance tuning;

clarified signature: more comprehensive operations;

clarified signature: more explicit types;

clarified signature: emphasize physical db files;

tuned: afford untyped/unscoped update;

clarified signature: avoid ill-defined type java.net.URL;

unused;

tuned: afford untyped/unscoped update;

more robust default: Scala imposes explicit "threads" value on ML, both the Poly/ML RTS and Isabelle/ML;

clarified signature: more explicit types/scopes;

tuned names;

tuned;

tuned documentation;

more robust: disallow empty clusters, so "isabelle build -H" really means cluster build;

clarified modules: centralize default policy;

more explicit types --- fewer warnings in IntelliJ IDEA;

tuned: avoid shadowing of names;

clarified default "isabelle build -j0 -H";

tuned whitespace;

clarifier worker vs. master, which may coincide for local build;

clarified signature: more standard defaults;

clarified signature;

clarified signature;

tuned;

prefer static object, while class is required for "services";

clarified signature: prefer default;

merged

tuned;

more robust: check subclasses as well;

more robust;

support for alternative user home, e.g. to avoid slow NFS shares;

support explicit USER_HOME within SSH session;

tuned;

merged

Further adjustments to the syntax for Lebesgue integration

tuned comments;

more robust: always close, despite failure;

clarified signature;

tuned signature;

tuned comments;

clarified signature;

Distinguish two versions of cvc5 -- one used for Sledgehammer, one for proof reconstruction in SMT. provided by Mathias Fleury

tuned whitespace;

prefer static object, while class is required for "services" (see 47eb96592aa2);

clarified directories; clarified names;

tuned signature;

tuned: prefer explicit update operation for immutable options;

tuned message;

more robust type, with explicit default;

tuned usage message;

clarified signature;

more robust defaults;

merged

added lemmas relpow_trans[trans] and relpowp_trans[trans]

more on disjunctive addition/subtraction

merged