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;

merged

simplified proofs

more rules for ordered real vector spaces

simplified setup

tuned proof

merged

enable share_common_data for "isabelle dump" and its derivatives (e.g. "isabelle mmt_import"): this has the potential to reduce ML heap size considerably, after initial command definitions;

support for share_common_data after define_command and before actual update: this affects string particles of command tokens;

more scalable -- less ML heap requirements;

tuned whitespace;

Integrate locale activation fallback diagnostics with 'trace_locales'.

entry point for analysis without integration theory

removed Brouwer_Fixpoint from imports of Derivative

removed unused lemma, generalized, reduced dependencies

fixed typo

moved lemmas; reduced dependencies of Lipschitz

explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space

merged

moved lemmas

moved basic theorem

proper positions for 'termination' command (see also 5549e686d6ac);

tuned names -- proper scopes;

added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);

proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;

Tracing of locale activation.

tuned

always export Pure proofs;

clarified 'thm_deps' command;

more compact: avoid pointless PThm rudiments;

clarified signature: prefer total operations;

proper graph traversal: avoid multiple visit of unnamed nodes;

more scalable: avoid huge intermediate XML elems;

more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;

NEWS;

merged

export thm_deps;

proper theory context;

clarified thm_id vs. thm_node/thm: retain theory_name; support for thm_deps: expand unnamed nodes;

clarified signature;

tuned;

unused (see 095dadc62bb5);

tuned;

tuned signature;