eliminated ASCII syntax from Pure bootstrap; tuned comments;

merged

new material on matrices, etc., and consolidating duplicate results about of_nat

notation for dummy sort;

more symbols;

merged

tuned signature;

tuned signature;

tuned signature;

removed unused clone of (map o apsnd); removed unused variant of HOLogic.mk_obj_eq;

prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS;

added HOLogic.mk_obj_eq convenience and eliminated some clones;

tuned -- use existing Morphism.instantiate_morphism;

Merged;

merged

Unified the order of zeros and poles; improved reasoning around non-essential singularites

merged

tuned;

tuned signature -- eliminated clones;

command 'interpret' no longer exposes resulting theorems as literal facts;

more robust normalization of witness, e.g. relevant for proofs of transfer_existence_ivl0, transfer_flow0 in AFP/thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy;

tuned;

more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;

explicit operations to instantiate frees: typ, term, thm, morphism;

more operations for ctyp, cterm;

minor tuning and clarification;

minor tuning and clarification;

tuned signature;

fixed the proof of pair_measure_count_space

merged

fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring

merged

type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0

simplified Radix_Sort

merged

merged

moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

simplified def of stable

Lots of new material about matrices, etc.

tuned proofs -- prefer explicit names for facts from 'interpret';

merged

eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);

tuned signature;

tuned;

use lazy notes for locale context init and later additions of facts;

avoid premature Lazy.force due to strict "?" operator;

Merge

Merge

lots of new material, ultimately related to measure theory

merged

support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes; register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel); support for lazy notes for locale activation (still inactive);

tuned;

tuned: more parallel;

clarified modules;

clarified modules;

tuned;

tuned;

tuned signature;

tuned: more accurate transfer;

store facts as lazy values;

clarified operations;

misc tuning and clarification;

clarified signature;

clarified modules;

more operations;

added lemma

tuned;

clarified signature;

misc tuning and clarification; removed unused all_registrations_of;

clarified signature;

more explicit instantiate_morphism (without checks for typ / term component);

tuned;

tuned signature;

more thorough jEdit.propertiesChanged(), which includes KeymapManager.reload() and jEdit.initKeyBindings();

avoid conflict with Isabelle/jEdit completion of '>', e.g. "-->", "==>";

trim context of persistent data;

trim context of persistent data;

trim context of persistent data;

clarified apply_transaction: always continue without presentation context;

more tight presentation context: avoid storing full Toplevel.state;

tuned;

more informative theories_trace;

merged

tuned signature (again);

trim context of persistent data;

trim context of persistent data;

proper file name;

trim context of persistent data; tuned signature;

clarified data operations, with trim_context and transfer;

tuned;

trim context of persistent data; tuned;

trim context of persistent data;

removed unused material;

trim context of persistent data;

trim context of persistent data; no need to trim context for del operations;

tuned;

tuned whitespace;

more operations;

optional trace of created theory values;

more operations;

auxiliary operation for space profiling;

special treatment of 0 only refers to type char

merged

features and caveats of datatype_record

merged

strengthen filter relator to canonical categorical definition with better properties

recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;

merged

more symbols;

New theory ex/Radix_Sort.thy

records based on datatypes/BNF infrastructure

updated polyml component;

no --enable-shared: leads to slow bigint operations (e.g. in session HOL-ODE-Examples);

retain remote_builds_old for build_status;

lxbroy7 no longer exists;

added lemmas

corrected some URLs

permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc;

merged

updated polyml component -- omitting bad polyml-5.7.1-3;