2016-12-12 ago merged
2016-12-12 ago proper session HOL-Types_To_Sets;
2016-11-01 ago back to post-release mode -- after fork point;
2016-10-31 ago moved contribution to right release
2016-10-25 ago tuned and updated for release;
2016-10-24 ago added Nunchaku integration
2016-10-24 ago Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
2016-10-07 ago updated for release;
2016-10-03 ago CONTRIBUTORS
2016-09-29 ago CONTRIBUTORS: new proof method "argo"
2016-07-27 ago NEWS: Primes
2016-07-07 ago got rid of class cmp; added height-size proofs by Daniel Stuewe
2016-06-08 ago NEWS and CONTRIBUTORS for SPMF
2016-03-28 ago tuning
2016-03-22 ago document addition of 'corec'
2016-03-18 ago move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-03 ago constructive formulation of factorization
2016-02-17 ago prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-02-12 ago merged
2016-01-24 ago more CONTRIBUTORS;
2016-01-20 ago back to post-release mode -- after fork point;
2016-01-19 ago tuned;
2016-01-19 ago Added approximation of powr to NEWS/CONTRIBUTORS
2016-01-12 ago crediting LCP in CONTRIBUTORS
2016-01-10 ago print_record NEWS and CONTRIBUTORS
2016-01-08 ago tuned;
2016-01-07 ago Added formal power series updates to NEWS/CONTRIBUTORS
2016-01-06 ago misc tuning for release;
2016-01-06 ago add the proof of the central limit theorem
2016-01-05 ago misc tuning for release;
2016-01-05 ago Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
2015-12-31 ago misc updates for release;
2015-12-19 ago documentation on last state of the art concerning interpretation
2015-12-01 ago add formalisation of Bourbaki-Witt fixpoint theorem
2015-11-02 ago Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-08-12 ago NEWS, CONTRIBUTORS, documentation for lift_bnf
2015-07-27 ago formal class for factorial (semi)rings
2015-07-08 ago moved normalization and unit_factor into Main HOL corpus
2015-07-02 ago more CONTRIBUTORS;
2015-06-19 ago separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
2015-06-12 ago CONTRIBUTORS
2015-05-25 ago merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
2015-05-04 ago tuned;
2015-05-04 ago CONTRIBUTORS
2015-04-19 ago back to post-release mode -- after fork point;
2015-04-17 ago added Eisbach, using version 3752768caa17 of its Bitbucket repository;
2015-04-11 ago updated for release;
2015-04-08 ago misc tuning for release;
2015-03-25 ago more multiset theorems
2014-12-05 ago add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
2014-10-08 ago move Code_Test to HOL/Library;
2014-09-06 ago theory about lexicographic ordering on functions
2014-08-22 ago generic euclidean algorithm (due to Manuel Eberl)
2014-08-10 ago merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
2014-08-09 ago tuned;
2014-07-30 ago CONTRIBUTORS;
2014-07-27 ago back to post-release mode -- after fork point;
2014-07-05 ago CONTRIBUTORS
2014-07-05 ago tuned;
2014-07-05 ago added Tom's hyp_subst update