src/HOL/Library/Library.thy
2017-04-06 haftmann 2017-04-06 session containing computational algebra
2017-02-26 haftmann 2017-02-26 re-established AFP entry for FinFuns as library
2016-12-17 haftmann 2016-12-17 clarified library contents
2016-09-30 hoelzl 2016-09-30 Library: fix name Product_plus to Product_Plus
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Product_Vector and Inner_Product from Library
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Continuum_Not_Denumerable from Library
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
2016-09-29 eberlm 2016-09-29 Set_Permutations replaced by more general Multiset_Permutations
2016-09-15 Lars Hupel 2016-09-15 new type for finite maps; use it in HOL-Probability
2016-09-01 wenzelm 2016-09-01 clarified session; misc tuning and modernization;
2016-07-12 wenzelm 2016-07-12 more standard name;
2016-07-04 haftmann 2016-07-04 combinator to build partial equivalence relations from a predicate and an equivalenc relation
2016-07-04 haftmann 2016-07-04 basic facts about almost everywhere fix bijections
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-05-24 eberlm 2016-05-24 Added set permutations/random permutations
2016-05-04 hoelzl 2016-05-04 move Stirling numbers from AFP/Discrete_Summation
2016-03-22 blanchet 2016-03-22 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
2016-03-18 Andreas Lochbihler 2016-03-18 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-02-09 hoelzl 2016-02-09 add extended nonnegative real numbers
2016-02-18 hoelzl 2016-02-18 add countable complete lattices
2016-02-17 haftmann 2016-02-17 separated potentially conflicting type class instance into separate theory
2015-12-01 Andreas Lochbihler 2015-12-01 add formalisation of Bourbaki-Witt fixpoint theorem
2015-09-15 lammich 2015-09-15 Omega_Words_Fun: Infinite words as functions from nat.
2015-07-16 hoelzl 2015-07-16 move disjoint sets to their own theory
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-04-06 nipkow 2015-04-06 new theory Library/Tree_Multiset.thy
2015-03-25 blanchet 2015-03-25 more multiset theorems
2014-10-29 wenzelm 2014-10-29 more standard theory name;
2014-10-08 hoelzl 2014-10-08 add Linear Temporal Logic on Streams
2014-10-08 Andreas Lochbihler 2014-10-08 move Code_Test to HOL/Library; add corresponding entries in NEWS and CONTRIBUTORS
2014-10-07 hoelzl 2014-10-07 move Stream theory from Datatype_Examples to Library
2014-09-07 haftmann 2014-09-07 explicit theory with additional, less commonly used list operations
2014-09-06 haftmann 2014-09-06 theory about sum and product on function bodies
2014-09-06 haftmann 2014-09-06 theory about lexicographic ordering on functions
2014-09-01 blanchet 2014-09-01 took out legacy material from 'HOL/Library/Library.thy'
2014-08-28 blanchet 2014-08-28 renaming theory 'Old_SMT'
2014-08-28 blanchet 2014-08-28 moved old 'smt' method out of 'Main'
2014-08-19 Andreas Lochbihler 2014-08-19 rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
2014-06-12 nipkow 2014-06-12 new theory of binary trees
2014-05-29 nipkow 2014-05-29 removed Kleene_Algebra because of superior AFP entry; authors agreed
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-13 traytel 2014-05-13 bnf_decl -> bnf_axiomatization
2014-04-05 haftmann 2014-04-05 proper inclusion into library
2014-03-10 hoelzl 2014-03-10 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
2014-01-29 paulson 2014-01-29 Replacing the theory Library/Binomial by Number_Theory/Binomial
2014-01-24 blanchet 2014-01-24 killed 'More_BNFs' by moving its various bits where they (now) belong
2014-01-20 blanchet 2014-01-20 dissolved BNF session
2014-01-16 blanchet 2014-01-16 moved 'Zorn' into 'Main', since it's a BNF dependency
2014-01-16 blanchet 2014-01-16 adapted to move of Wfrec
2013-11-26 hoelzl 2013-11-26 Add Zorn to HOL-Library
2013-11-20 blanchet 2013-11-20 effectively reverted d25fc4c0ff62, to avoid quasi-cyclic dependencies with HOL-Cardinals and minimize BNF dependencies
2013-10-31 haftmann 2013-10-31 more convenient place for a theory in solitariness
2013-10-31 haftmann 2013-10-31 consolidated clone theory
2013-09-27 kuncar 2013-09-27 new theory of finite sets as a subtype
2013-05-27 wenzelm 2013-05-27 actually test theory Order_Union;
2013-04-09 hoelzl 2013-04-09 move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-03-26 wenzelm 2013-03-26 tuned imports;
2013-03-09 haftmann 2013-03-09 discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
2013-03-05 nipkow 2013-03-05 New theory of infinity-extended types; should replace Extended_xyz eventually