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