src/HOL/Library/Library.thy
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
2013-02-24 haftmann 2013-02-24 turned example into library for comparing growth of functions
2013-02-17 haftmann 2013-02-17 fundamentals about discrete logarithm and square root
2013-02-15 haftmann 2013-02-15 attempt to re-establish conventions which theories are loaded into the grand unified library theory; four different code generation tests for different code setup constellations; augment code generation setup where necessary
2012-11-20 hoelzl 2012-11-20 add Countable_Set theory
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards
2012-08-09 wenzelm 2012-08-09 explicit FIXME;
2012-07-31 kuncar 2012-07-31 implementation of sets by RBT trees for the code generator
2012-07-22 haftmann 2012-07-22 library theories for debugging and parallel computing using code generation towards Isabelle/ML
2012-07-17 haftmann 2012-07-17 explicitly import Dlist theory into library
2012-07-05 haftmann 2012-07-05 Stub theory for division on functionals.
2012-05-29 Andreas Lochbihler 2012-05-29 move FinFuns from AFP to repository
2012-03-30 haftmann 2012-03-30 dropped now obsolete Cset theories
2011-12-26 haftmann 2011-12-26 incorporated More_Set and More_List into the Main body -- to be consolidated later
2011-12-04 huffman 2011-12-04 remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
2011-09-25 haftmann 2011-09-25 Quotient_Set.thy is part of library
2011-09-12 bulwahn 2011-09-12 moving connection of association lists to Mappings into a separate theory
2011-09-07 haftmann 2011-09-07 theory of saturated naturals contributed by Peter Gammie
2011-08-28 haftmann 2011-08-28 avoid loading List_Cset and Dlist_Cet at the same time
2011-08-17 wenzelm 2011-08-17 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
2011-08-16 huffman 2011-08-16 get Library/Permutations.thy compiled and working again
2011-08-02 krauss 2011-08-02 moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy