src/HOL/Library/Library.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
2009-10-30 haftmann 2009-10-30 moved Commutative_Ring into session Decision_Procs
2009-10-26 haftmann 2009-10-26 re-moved theory Fin_Fun to AFP
2009-10-26 haftmann 2009-10-26 merged
2009-10-23 himmelma 2009-10-23 distinguished session for multivariate analysis
2009-10-23 haftmann 2009-10-23 turned off old quickcheck
2009-09-01 haftmann 2009-09-01 some reorganization of number theory
2009-07-10 krauss 2009-07-10 move Kleene_Algebra to Library
2009-06-29 haftmann 2009-06-29 renamed theory Code_Set to Fset
2009-06-25 haftmann 2009-06-25 added List_Set and Code_Set theories
2009-06-23 chaieb 2009-06-23 Added Library/Fraction_Field.thy: The fraction field of any integral domain
2009-06-02 haftmann 2009-06-02 added Fin_Fun theory
2009-06-02 berghofe 2009-06-02 Added Convex_Euclidean_Space.thy again.
2009-05-28 himmelma 2009-05-28 Removed Convex_Euclidean_Space.thy from Library.
2009-05-28 himmelma 2009-05-28 Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
2009-05-16 haftmann 2009-05-16 experimental move of Quickcheck and related theories to HOL image
2009-05-12 chaieb 2009-05-12 Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
2009-05-07 haftmann 2009-05-07 added theory for explicit equivalence relation in preorders
2009-03-06 haftmann 2009-03-06 constructive version of Cantor's first diagonalization argument
2009-03-04 chaieb 2009-03-04 Added Libray dependency on Topology_Euclidean_Space
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-20 huffman 2009-02-20 add theory of products as real vector spaces to Library
2009-02-20 huffman 2009-02-20 add new theory Product_plus.thy to Library
2009-02-19 huffman 2009-02-19 add formalization of a type of integers mod 2 to Library
2009-02-19 huffman 2009-02-19 new theory of real inner product spaces
2009-02-18 huffman 2009-02-18 move Polynomial.thy to Library
2009-02-18 huffman 2009-02-18 move FrechetDeriv.thy to Library