src/HOL/Library/Library.thy
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 http://www.cs.ru.nl/~freek/100/)
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.
2005-04-14 nipkow 2005-04-14 Removed dir Orderings in Library
2005-01-26 nipkow 2005-01-26 added OptionalSugar
2004-11-24 berghofe 2004-11-24 Added EfficientNat
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-05-06 wenzelm 2004-05-06 tuned document;
2004-03-29 skalberg 2004-03-29 Added bitvector library (Word) to HOL/Library and a theory using it (Adder) to HOL/ex.
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2003-11-24 paulson 2003-11-24 conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field
2003-07-24 paulson 2003-07-24 new theory NatPair of the injection from nat*nat -> nat
2001-06-09 wenzelm 2001-06-09 tuned Primes theory;
2001-05-31 oheimb 2001-05-31 added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-02-04 wenzelm 2001-02-04 added Permutation;
2001-01-26 nipkow 2001-01-26 Merged Example into While_Combi
2001-01-20 wenzelm 2001-01-20 Ring_and_Field_Example;
2001-01-19 wenzelm 2001-01-19 added HOL/Library/Nested_Environment.thy;
2000-12-06 wenzelm 2000-12-06 activate Rational_Numbers;
2000-12-06 wenzelm 2000-12-06 deactivate Rational_Numbers (tmp!);
2000-12-06 wenzelm 2000-12-06 Rational_Numbers;
2000-11-17 wenzelm 2000-11-17 Ring_and_Field;
2000-10-25 wenzelm 2000-10-25 added List_Prefix;
2000-10-18 wenzelm 2000-10-18 "The Supplemental Isabelle/HOL Library";