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
2007-06-01 nipkow 2007-06-01 Moved list comprehension into List
2007-05-25 nipkow 2007-05-25 Added List_Comprehension
2007-05-15 chaieb 2007-05-15 A verified theory for rational numbers representation and simple calculations; verified with respect to the real numbers;
2007-04-26 haftmann 2007-04-26 moved code generation pretty integers and characters to separate theories
2007-03-26 haftmann 2007-03-26 importing Eval theory
2007-02-26 krauss 2007-02-26 Added formalization of size-change principle (experimental).
2006-12-04 krauss 2006-12-04 added Ramsey.thy to Library imports, to include it in the daily builds
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-11-06 haftmann 2006-11-06 added state monad to HOL library
2006-10-01 wenzelm 2006-10-01 moved theory Infinite_Set to Library;
2006-08-21 haftmann 2006-08-21 added some codegen examples/applications
2006-05-09 haftmann 2006-05-09 added ExecutableRat.thy
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
2006-04-26 kleing 2006-04-26 moved arithmetic series to geometric series in SetInterval
2006-04-07 kleing 2006-04-07 renamed ASeries to Arithmetic_Series, removed the ^M
2006-03-10 schirmer 2006-03-10 Added Library/AssocList.thy
2006-02-19 kleing 2006-02-19 * added Library/ASeries (sum of arithmetic series with instantiation to nat and int) * added Complex/ex/ASeries_Complex (instantiation of the above for reals) * added Complex/ex/HarmonicSeries (should really be in something like Complex/Library) (these are contributions by Benjamin Porter, numbers 68 and 34 of
2005-12-13 wenzelm 2005-12-13 added HOL/Library/Coinductive_List.thy;
2005-09-25 berghofe 2005-09-25 Added ExecutableSet.
2005-09-20 wenzelm 2005-09-20 added Commutative_Ring (from Main HOL);
2005-08-01 obua 2005-08-01 1. changed configuration variables for linear programming (Cplex_tools): LP_SOLVER is either CPLEX or GLPK CPLEX_PATH is the path to the cplex binary GLPK_PATH is the path to the glpk binary The change makes it possible to switch between glpk and cplex at runtime. 2. moved conflicting list theories out of Library.thy into ROOT.ML
2005-07-25 avigad 2005-07-25 Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
2005-05-29 obua 2005-05-29 Removes an inconsistent definition from Library.thy , so that the lexical order is the standard order for lists. The prefix order is not built any more.