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

proper session dirs;

tuned signature;

tuned;

merged;

Added tag Isabelle2018-RC4 for changeset 34b8ff7cb109

updated for release;

updated screenshot;

updated documentation;

suppress verit-2016post -- not ready for release;

isabelle build options -c -x -B refer to imports_graph;

more uniform checks;

tuned signature;

tuned signature;

tuned signature;

clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;

tuned signature;

export shyps as regular typargs;

more uniform facts: single vs. multi;

explicit names for bound variables;

export in foundational order;

recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;