clarified Load_State / load_limit;

clarified Load_State;

discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;

count nodes uniformly: avoid overloaded session;

clarified signature;

simplified proof

tuned signature;

clarified signature: more options;

clarified signature: read full session requirements;

clarified signature;

tuned signature;

clarified options -- more scalable;

obsolete;

proper replacement for (map_types (K dummyT));

Term_XML.Encode/Decode.term uses Const "typargs";

prefer atomic edits -- potentially more robust;

clarified signature -- potentially more robust;

just one dump_checkpoint Main -- potentially more robust;

more robust: avoid update/interrupt of long-running print_consolidation;

avoid censorship of options, e.g. relevant for Isabelle/MMT to provide its own value;

consolidate less aggressively: avoid live-lock when PIDE round-trip takes too long (e.g. in complex theory hierarchies);

obsolete (see 60abd1e94168);

more robust after shutdown;

more sequential access to Session.manager.global_state: avoid minor divergence of tip version;

clarified share_common_data: after finished checkpoint, before next edits;

obsolete (see 030a6baa5cb2 and d14ddb1df52c);

support headless_load_limit for more scalable load process;

added dump_options: disabled by default;

tuned message;

clarified incremental loading: requirements based on maximal nodes;

tuned signature;

tuned;

tuned message;

more explicit type Load_State;

more operations -- incremental exploration of reachable nodes;

tuned messages (again) -- avoid confusion wrt. total remaining size;

added lemma

more Phabricator configuration;

A little more material from the Fourier AFP entry, and the correction of two very slow proof lines

boot with Phabricator PHP daemon;

clarified sshd setup: standard service on non-standard port 222, special "vcs" service on standard port 22;

disable lrzcloud1 -- superseded by lrzcloud2;

merged

replaced new type ('a,'b) tree by old type ('a*'b) tree.

more Phabricator configuration;

merged

merged

simplified proofs

some information about Phabricator server setup;

More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.

merged

Enforced precodition "n <= length xs" to avoid relying on "hd []".

Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)

tuned

added lemma

proper file name instead of font name (amending dc9a39c3f75d);

added function

merged

clarified data structures; eliminated presumably obsolete check of known_theories: should be unique by construction;

unused;