typo

merged

tuned signature;

added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x

merged

merged

tiny cleanup

merged

A few new results, elimination of duplicates and more use of "pairwise"

tuned

tuned "=" syntax declarations; made "~=" uniformly "infix"

tuned proof

simplified defns

"undefined" not needed, [] is perfectly natural

tuned

tuned

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

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;

clarified signature;

clarified signature;

clarified signature;

trim nodes_status: avoid potential memory leak;

simplified (cf. dcd69422b953);

clarified modules;

clarified modules;

Finite_Map: monotonicity

State_Monad: more simp lemmas

enforce ML_system_64: more robust as cold build, without command_timings;

clarified signature;

removed obsolete RC tags;

(re)moved lemmas

updated to renaming

updated common hosts;

merged

Added tag Isabelle2018 for changeset 91162dd89571

merged

canonical session directories in correspondence to Known.files;

Zorn's lemma for relations defined by predicates

merged