2007-08-20 ago boolean algebras as locales and numbers as types by Brian Huffman
2007-08-15 ago added Eval_Witness theory
2007-08-09 ago proper implementation of rational numbers
2007-07-19 ago uniform naming conventions for CG theories
2007-06-01 ago Moved list comprehension into List
2007-05-25 ago Added List_Comprehension
2007-05-15 ago A verified theory for rational numbers representation and simple calculations;
2007-04-26 ago moved code generation pretty integers and characters to separate theories
2007-03-26 ago importing Eval theory
2007-02-26 ago Added formalization of size-change principle (experimental).
2006-12-04 ago added Ramsey.thy to Library imports, to include it in the daily builds
2006-11-08 ago moved theories Parity, GCD, Binomial to Library;
2006-11-06 ago added state monad to HOL library
2006-10-01 ago moved theory Infinite_Set to Library;
2006-08-21 ago added some codegen examples/applications
2006-05-09 ago added ExecutableRat.thy
2006-05-05 ago First usable version of the new function definition package (HOL/function_packake/...).
2006-04-26 ago moved arithmetic series to geometric series in SetInterval
2006-04-07 ago renamed ASeries to Arithmetic_Series, removed the ^M
2006-03-10 ago Added Library/AssocList.thy
2006-02-19 ago * added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
2005-12-13 ago added HOL/Library/Coinductive_List.thy;
2005-09-25 ago Added ExecutableSet.
2005-09-20 ago added Commutative_Ring (from Main HOL);
2005-08-01 ago 1. changed configuration variables for linear programming (Cplex_tools):
2005-07-25 ago Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
2005-05-29 ago Removes an inconsistent definition from Library.thy ,
2005-04-14 ago Removed dir Orderings in Library
2005-01-26 ago added OptionalSugar
2004-11-24 ago Added EfficientNat
2004-08-18 ago import -> imports
2004-08-16 ago New theory header syntax.
2004-05-06 ago tuned document;
2004-03-29 ago Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
2004-01-27 ago replacing HOL/Real/PRat, PNat by the rational number development
2003-11-24 ago conversion of integers to use Ring_and_Field;
2003-07-24 ago new theory NatPair of the injection from nat*nat -> nat
2001-06-09 ago tuned Primes theory;
2001-05-31 ago added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-02-04 ago added Permutation;
2001-01-26 ago Merged Example into While_Combi
2001-01-20 ago Ring_and_Field_Example;
2001-01-19 ago added HOL/Library/Nested_Environment.thy;
2000-12-06 ago activate Rational_Numbers;
2000-12-06 ago deactivate Rational_Numbers (tmp!);
2000-12-06 ago Rational_Numbers;
2000-11-17 ago Ring_and_Field;
2000-10-25 ago added List_Prefix;
2000-10-18 ago "The Supplemental Isabelle/HOL Library";