proper build_selection for clean_build (amending 961285f581e6): e.g. relevant for "isabelle build_doc";

clarified signature (again);

clarified exclusion: operate on completed selection, as last step;

tuned;

tuned signature;

clarifified selection: always wrt. build_graph structure; tuned signature;

tuned;

tuned signature;

more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)

integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)

added FIXMEs

Replaced { } proofs by local lemmas; added Hoare logic with logical variables.

backed out odd "bug fix" 671decd2e627;

more recent polyml-test version; afford more heap by default: all platforms are now 64bit and presumably have sufficient memory;

minimal document model for theory files;

tuned signature;

tuned signature;

more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);

uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");

updated comments;

updated to scala-2.12.4;

testing NewTestRegisterSave;

superseded by plain_identify;

tolerate odd negative times from old log files (before 1698e9ccef2d);

prefer main entry points of HOL;

tuned signature;

clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;

more robust sorted_entries;

more convenient build_log_history;

tuned;

more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;

polyml-test version based on experimental branch NewTestRegisterSave;

support for libgmp on x86_64-darwin;

avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;

delegate boundary cases to existing IntInf.pow;

plain identify job for Isabelle + AFP, independent of any Isabelle technology;

tuned (non-unique example);

clarified situation of global theory names;

less global theories -- avoid confusion about special cases;

proper deps;

allow unrelated ancestor; clarified error;

tuned;

support alternative ancestor session;

support focus_session, for much faster startup of Isabelle/jEdit; more options for "isabelle jedit";

more timing;

tuned;

init only once (see also c0f776b661fa);

proper merge (amending fb46c031c841);

build faster without heap images for minor imports;

proper order for entries from multiple profiles, notably "AFP";

tuned output;

tuned;

logic_selector refers to raw logic name;

clarified terminology;

tuned signature;

do not store bulky Session.Deps;

avoid duplicate invocation of expensive Sessions.deps on full_sessions; tuned;

added isabelle jedit options -B, -P, clarified -R; misc tuning and clarification;

no heap sharing for empty session (e.g. HOL-ODE);

tuned diagram;