clarified modules;

tuned -- more direct ML expressions;

tuned whitespace;

more accurate treatment of propositions within proof terms, but these are…

unused;

document antiquotations + clarify porting text slightly

merge

add a section about Stellar's intact sets

Add lemma strong_cluster_union

Remove spurious W variable in locale assumption

updated veriT part of Sledgehammer documentation

added para constrasting 'primrec' and 'fun' -- and removed my middle name

dedicated fact collections for algebraic simplification rules potentially…

avoid sign_simps in favour of algebra_split_simps

merged

misc tuning and clarification;

tuned;

tuned;

tuned -- allow slightly more expensive atomic proofs;

tuned;

clarified signature -- some operations to support fully explicit proof terms;

tuned;

proper treatment of sorts;

tuned app_types: more direct map_proof_types_same;

tuned;

generalized parsing, for e.g. Leo-III

Moved some lemmas about limits to Complex_Main

More theorems about limits, including cancellation simprules

Generalised two results concerning limits from the real numbers to type classes

formally augmented corresponding rules for field_simps

formally augmented corresponding rules for field_simps

updated to work with recent automata changes

added NGBA implementations

adjusted NBA implementation

added NBA combination nodes theorems, minor adjustments

clarified option type;

count document nodes via raw file length;

refer to explicit ISABELLE_DOT instead of implicit PATH;

merged

clarified Load_State;

clarified Load_State / load_limit;

discontinued pointless dump_checkpoint and share_common_data -- superseded by…

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;

avoid name clash of internal derivations;

avoid name clash of internal derivations;

proper Consts.dummy_types;

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…

consolidate less aggressively: avoid live-lock when PIDE round-trip takes too…

obsolete (see 60abd1e94168);

more robust after shutdown;

more sequential access to Session.manager.global_state: avoid minor divergence…

clarified share_common_data: after finished checkpoint, before next edits;

support headless_load_limit for more scalable load process;

obsolete (see 030a6baa5cb2 and d14ddb1df52c);

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;

updated to devel

added lemma