src/HOL/Library/Library.thy
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
2011-07-26 Andreas Lochbihler 2011-07-26 Add theory for setting up monad syntax for Cset
2011-07-25 bulwahn 2011-07-25 removing SML_Quickcheck
2011-07-19 hoelzl 2011-07-19 rename Nat_Infinity (inat) to Extended_Nat (enat)
2011-06-07 bulwahn 2011-06-07 splitting Cset into Cset and List_Cset
2011-06-02 bulwahn 2011-06-02 splitting Dlist theory in Dlist and Dlist_Cset
2011-06-01 bulwahn 2011-06-01 splitting RBT theory into RBT and RBT_Mapping
2011-01-08 wenzelm 2011-01-08 renamed Sum_Of_Squares to Sum_of_Squares;
2010-11-22 haftmann 2010-11-22 merged
2010-11-22 haftmann 2010-11-22 replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-22 bulwahn 2010-11-22 adding Enum to HOL-Main image and removing it from HOL-Library
2010-11-03 haftmann 2010-11-03 moved theory Quicksort from Library/ to ex/
2010-08-20 haftmann 2010-08-20 split and enriched theory SetsAndFunctions
2010-07-14 haftmann 2010-07-14 load cache_io before code generator; moved adhoc-overloading to generic tools
2010-07-13 krauss 2010-07-13 uniform do notation for monads
2010-07-13 krauss 2010-07-13 generic ad-hoc overloading via check/uncheck
2010-07-02 haftmann 2010-07-02 remove codegeneration-related theories from big library theory
2010-07-01 hoelzl 2010-07-01 Add theory for indicator function.
2010-05-20 haftmann 2010-05-20 added theory More_List
2010-05-17 haftmann 2010-05-17 dropped old Library/Word.thy and toy example ex/Adder.thy