prefer define_commands_bulk: fewer protocol messages;

clarified signature;

tuned signature -- prefer bulk messages;

tuned signature;

proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);

more robust;

unused;

proper finished_theory status for result;

more central checkpoint;

disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;

merged

load theories in stages, to reduce ML heap requirements;

more complete graph;

tuned messages;

tuned signature;

clarified signature;

tuned important special case;

tuned signature;

more dump_checkpoints;

clarified signature;

clarified state variable: avoid extra mutability via Promise;

Removal of the redundant ancestor Continuous_Extension

Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.

Theory Derivative no longer depends on Path_Connected

more explicit type Dump.Session, with context information;

proper orientation;

clarified signature: prefer operations without position;

prefer Theory_Ordering theory names are unique (due to proper session context);

clarified signature: full dependency graph;

merged

more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;

tuned signature;