tuned -- allow slightly more expensive atomic proofs;

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

tuned;

tuned;

proper treatment of sorts;

tuned app_types: more direct map_proof_types_same;

tuned;

generalized parsing, for e.g. Leo-III

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

clarified option type;

count document nodes via raw file length;

merged

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;