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