src/HOL/Library/Library.thy
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
2010-05-04 hoelzl 2010-05-04 Add Convex to Library build
2010-04-15 haftmann 2010-04-15 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
2010-03-13 wenzelm 2010-03-13 removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
2010-03-06 haftmann 2010-03-06 added Table.thy
2010-02-22 haftmann 2010-02-22 added Dlist
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.
2010-02-10 wenzelm 2010-02-10 renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
2010-02-10 haftmann 2010-02-10 revert uninspired Structure_Syntax experiment
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures
2010-02-08 haftmann 2010-02-08 separate theory for index structures
2009-12-07 haftmann 2009-12-07 merged Crude_Executable_Set into Executable_Set
2009-12-02 haftmann 2009-12-02 added Crude_Executable_Set.thy
2009-11-12 bulwahn 2009-11-12 added a tabled implementation of the reflexive transitive closure