src/HOL/Library/Library.thy
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
2009-02-18 huffman 2009-02-18 split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
2009-02-12 nipkow 2009-02-12 Moved FTA into Lib and cleaned it up a little.
2009-02-09 chaieb 2009-02-09 added Determinants to Library
2009-02-09 chaieb 2009-02-09 added Euclidean_Space and Glbs to Library
2009-02-09 chaieb 2009-02-09 Added HOL/Library/Finite_Cartesian_Product.thy to Library
2009-02-06 haftmann 2009-02-06 session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
2009-02-06 chaieb 2009-02-06 fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
2009-02-05 haftmann 2009-02-05 moved Random.thy to Library
2009-02-02 haftmann 2009-02-02 added Mapping.thy to Library
2009-01-29 chaieb 2009-01-29 Added Formal_Power_Series in imports
2009-01-28 haftmann 2009-01-28 Reflection.thy now in HOL/Library
2009-01-16 haftmann 2009-01-16 moved Univ_Poly to Library
2009-01-08 haftmann 2009-01-08 split of Imperative_HOL theories from HOL-Library
2008-12-29 haftmann 2008-12-29 adapted HOL source structure to distribution layout
2008-12-10 nipkow 2008-12-10 moved ContNotDenum into Library
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-10-23 wenzelm 2008-10-23 fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
2008-09-16 haftmann 2008-09-16 evaluation using code generator
2008-09-02 nipkow 2008-09-02 Replaced Library/NatPair by Nat_Int_Bij.
2008-07-18 haftmann 2008-07-18 refined code generator setup for rational numbers; more simplification rules for rational numbers
2008-07-03 huffman 2008-07-03 add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-20 haftmann 2008-06-20 moved Float.thy to Library
2008-03-20 haftmann 2008-03-20 added theory Library/Enum.thy
2008-03-14 nipkow 2008-03-14 Added Order_Relation
2008-03-07 haftmann 2008-03-07 canonical order on option type
2008-03-03 krauss 2008-03-03 new theory of red-black trees, an efficient implementation of finite maps.
2008-02-28 wenzelm 2008-02-28 renamed ListSpace to ListVector;
2008-02-27 haftmann 2008-02-27 added theories for imperative HOL
2008-02-27 chaieb 2008-02-27 Loads Dense_Linear_Order.thy
2008-02-25 chaieb 2008-02-25 Uses Univ_Poly.thy
2008-01-14 nipkow 2008-01-14 *** empty log message ***
2007-11-06 wenzelm 2007-11-06 removed dependencies on Size_Change_Termination from HOL-Library;
2007-10-12 haftmann 2007-10-12 consolidated naming conventions for code generator theories
2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-09-18 nipkow 2007-09-18 Added function package to PreList Added sorted/sort to List Moved qsort from ex to Library
2007-09-06 berghofe 2007-09-06 Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories.
2007-08-20 kleing 2007-08-20 boolean algebras as locales and numbers as types by Brian Huffman
2007-08-15 haftmann 2007-08-15 added Eval_Witness theory
2007-08-09 haftmann 2007-08-09 proper implementation of rational numbers
2007-07-19 haftmann 2007-07-19 uniform naming conventions for CG theories