tuned

tuned

Removed problematic rules from continuous_intros

merged

tuned

tuned message (again);

proper binding positions within the defining command transaction;

smash position to avoid position of other file "~~/src/HOL/BNF_Composition.thy" (due to "bnf ID"), e.g. relevant for "HOL-Nominal-Examples.Class1";

clarified message;

tuned message;

clarified theory progress;

tuned message;

more robust test: virtualization may provide misleading information;

implicit use of NUMA policy, absorbing potential errors;

tuned signature;

tuned;

more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;

merged

ensure foundational order of commits, taking Pure as implicit starting point;

more accurate output;

clarified defaults; more uniform treatment of "disabled" case;

more accurate output;

support for watchdog_timeout;

tuned signature;

tuned signature;

removed junk;

tuned output;

more appropriate conversion of HOL character literals to character codes: symbolic newline is interpreted as 0x10

more explicit notion of ord value for HOL characters

left-over rename from 3f9bb52082c4

merged

continuously clean frontier of already committed theories: much less resource requirements;

tuned signature;

missing name

tuned whitespace;

merged

proper tast_context (amending 5f44ad150ed8);

clarified error progress and error_rc;

tuned signature;

clarified rc;

tuned signature;

dump aspects asynchronously;

record status of already committed nodes; tuned signature;

tuned;

tuned signature;

tuned;

added Let_def

merged

added int and real

simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;

setup option ML_system for special values that cannot be rebound within regular ML;

support dynamic commit of consilidated nodes; tuned signature;

tuned signature;

clarified Use_Theories_State;

tuned

merged

tuned doc

proper binding position for the resulting definition command, not this source file;

material on finite sets

support for watchdog_timeout;

tuned;

tuned;

tuned -- prefer immutable data;

tuned signature;

clarified Nodes_Status; tuned messages;

tuned

tuned

more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;

more detailed progress;

more informative node_status;

tuned signature;

more robust default options, notably for node consolidation;

tuned;

more robust: load_theories after consumer is installed;

merged

proper polarity of terminated status;

merged

tagged 1 theory: Great_Picard

tuned signature;

clarified signature;

tuned -- more robust against changes;

more robust: avoid race-condition of terminated vs. consolidated;

do not expose obscure flags;

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