15 months ago wenzelm 2018-03-01 clarified date for presentation vs. formal pull_date;
15 months ago wenzelm 2018-03-01 reveal raw data in CSV format;
15 months ago wenzelm 2018-03-01 support for CSV files;
16 months ago wenzelm 2018-03-01 tuned comment;
16 months ago wenzelm 2018-03-01 clarified syntax: reject formal comments explicitly, instead of ignoring them silently;
16 months ago immler 2018-02-28 merged
16 months ago immler 2018-02-28 generalized lemmas about orthogonal transformation
16 months ago wenzelm 2018-02-28 more explicit infixl (see initial 1edf0f223c6e); clarified name;
16 months ago wenzelm 2018-02-28 clarified use of vec type syntax;
16 months ago haftmann 2018-02-26 new lemma
16 months ago haftmann 2018-02-26 dedicated append function for string literals
16 months ago immler 2018-02-26 generalized
16 months ago immler 2018-02-26 moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
16 months ago wenzelm 2018-02-25 merged
16 months ago wenzelm 2018-02-25 prefer symbols;
16 months ago wenzelm 2018-02-25 tuned;
16 months ago wenzelm 2018-02-25 more abbrevs;
16 months ago wenzelm 2018-02-25 allow multiple entries of and_list (on both sides);
16 months ago wenzelm 2018-02-25 eliminated ASCII syntax from Pure bootstrap; tuned comments;
16 months ago paulson 2018-02-25 merged
16 months ago paulson 2018-02-25 new material on matrices, etc., and consolidating duplicate results about of_nat
16 months ago wenzelm 2018-02-25 notation for dummy sort;
16 months ago wenzelm 2018-02-24 more symbols;
16 months ago wenzelm 2018-02-23 merged
16 months ago wenzelm 2018-02-23 tuned signature;
16 months ago wenzelm 2018-02-23 tuned signature;
16 months ago wenzelm 2018-02-23 tuned signature;
16 months ago wenzelm 2018-02-23 removed unused clone of (map o apsnd); removed unused variant of HOLogic.mk_obj_eq;
16 months ago wenzelm 2018-02-23 prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS;
16 months ago wenzelm 2018-02-23 added HOLogic.mk_obj_eq convenience and eliminated some clones;
16 months ago wenzelm 2018-02-23 tuned -- use existing Morphism.instantiate_morphism;
16 months ago Wenda Li 2018-02-23 Merged;
16 months ago Wenda Li 2018-02-23 merged
16 months ago Wenda Li 2018-02-23 Unified the order of zeros and poles; improved reasoning around non-essential singularites
16 months ago wenzelm 2018-02-23 merged
16 months ago wenzelm 2018-02-23 tuned;
16 months ago wenzelm 2018-02-23 tuned signature -- eliminated clones;
16 months ago wenzelm 2018-02-23 command 'interpret' no longer exposes resulting theorems as literal facts;
16 months ago wenzelm 2018-02-23 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;
16 months ago wenzelm 2018-02-22 tuned;
16 months ago wenzelm 2018-02-21 more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;
16 months ago wenzelm 2018-02-21 explicit operations to instantiate frees: typ, term, thm, morphism;
16 months ago wenzelm 2018-02-21 more operations for ctyp, cterm;
16 months ago wenzelm 2018-02-21 minor tuning and clarification;
16 months ago wenzelm 2018-02-20 minor tuning and clarification;
16 months ago wenzelm 2018-02-20 tuned signature;
16 months ago paulson 2018-02-23 fixed the proof of pair_measure_count_space
16 months ago paulson 2018-02-23 merged
16 months ago paulson 2018-02-23 fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
16 months ago paulson 2018-02-22 merged
16 months ago paulson 2018-02-22 type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
16 months ago nipkow 2018-02-23 simplified Radix_Sort
16 months ago immler 2018-02-22 merged
16 months ago immler 2018-02-22 merged
16 months ago immler 2018-02-22 moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
16 months ago nipkow 2018-02-22 simplified def of stable
16 months ago paulson 2018-02-21 Lots of new material about matrices, etc.
16 months ago wenzelm 2018-02-20 tuned proofs -- prefer explicit names for facts from 'interpret';
16 months ago wenzelm 2018-02-20 merged
16 months ago wenzelm 2018-02-20 eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);