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;

clarified modules;