clarified quasi_consolidated state: ensure that exports are present for ok nodes;

clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;

tuned documentation;

more detailed node_status;

clarified bracketing of messages: [forked [running finished] joined];

NEWS;

clarified reset_notepad;

more robust reset_state: begin/end structure takes precedence over goal/proof structure;

no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;

clarified signature;

tuned;

clarified message;

updated version;

more explicit status for "canceled" command within theory node;

back to post-release mode;

clarified message;

more robust: memoize interrupt (e.g. resource problem) -- avoid multiple attempts;

more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);

tuned;

support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;

clarified signature: proper typargs;

merged

export locale content; read_theory_names: proper classrel, arities; tuned signature;

tuned;

Some basic materials on filters and topology

merged

more accurate position for auxiliary files;

clarified signature;

tuned;

more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442);

tuned;

tuned signature;

clarified signature;

clarified signature: explicit type Locale.registration;

tuned;

tuned;

updated URL to remote TPTP, following heads-up from Geoff Sutcliffe

prefer "locale begin ... end";

tuned signature;

support Thy_Element in Scala, following ML version;

tuned;

tuned;

tuned;

clarified signature;

tuned signature;

clarified modules;

tagged some theories

merged

systematic access to command ids;

more robust: Pure entities may lack id;

merged

tagged 21 theories in the Analysis library for the manual

tuned output;

Export.Provider for "isabelle dump" output_dir;

retain original id, which is command_id/exec_id for PIDE; tuned;

tuned signature;

tuned;

tuned signature;

clarified ML_environment: ML_write_global requires "Isabelle";

clarified signature: do not expose internal operation;

some NEWS (instead of proper documentation);

clarified signature;

simplified markup;

explicit setup of operations: avoid hardwired stuff;

clarified environment: allow "read>write" specification;

tuned;

tuned;

check environment name;

support named ML environments, notably "Isabelle", "SML"; more uniform options ML_read_global, ML_write_global; clarified bootstrap environment;

tuned;

tuned;

clarified signature;

clarified -- prefer new 'ML_export' command;

merged

material on finite maps

more uniform cartouche syntax; more documentation;

more uniform cartouche syntax;

more robust exit: avoid later Consolidate_Execution with handle_raw_edits (cf. 2fd3a6d6ba2e);

tuned message;

clarified message;

actually ensure globally unique counter results (amending a5853334c179);

retain original PolyML.pointerEq;

some modernization of notation

deprecation of ASCII syntax for indexed big operators

tuned

merged

tuned proofs

tuned

simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility

dropped redundant syntax translation rules for big operators

moved lemma from AFP

tuned lemmas

merged

tuned

prefer constructive primitive_part over implicit content_decompose

merged

tuned lemmas

more uniform parameter naming convention for choose and gchoose

slightly generalized theorems

tuned code setup

tuned

more theorems on fact

removed ineffective code equation

tuned whitespace

new simp rule

copied but not adapted

improved sectioning

merged

avoid session qualification because no tex is generated when used; tuned sectioning

removed ineffective code declarations

proper code abbreviation for power on real

tuned

tuned

suppress redundant messages;

optional notification of nodes_status (via progress); more accurate changed.nodes wrt. dep_theories; tuned signature;

tuned signature;

tuned;

tuned;

tuned signature;

tuned output;