2012-03-25 ago merged fork with new numeral representation (see NEWS)
2012-02-15 ago renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-11-23 ago modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-08-08 ago moved division ring stuff from Rings.thy to Fields.thy
2011-02-25 ago Some cleaning up
2010-08-28 ago formerly unnamed infix equality now named HOL.eq
2010-08-19 ago use antiquotations for remaining unqualified constants in HOL
2010-05-25 ago moved ML files where they are actually used;
2010-05-15 ago less pervasive names from structure Thm;
2010-05-07 ago renamed Normalizer to the more specific Semiring_Normalizer
2010-05-04 ago locale predicates of classes carry a mandatory "class" prefix
2010-03-18 ago now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-02-19 ago moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 ago moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 ago moved constants inverse and divide to Ring.thy
2010-02-08 ago dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-05 ago more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 ago new theory Algebras.thy for generic algebraic structures
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-04-29 ago farewell to class recpower
2009-04-05 ago fixed usage of rational constants
2009-03-27 ago merged
2009-03-27 ago normalized imports
2009-03-26 ago interpretation/interpret: prefixes are mandatory by default;
2009-03-22 ago distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
2009-03-16 ago simplified method setup;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-11 ago Updated paths in Decision_Procs comments and NEWS
2009-02-09 ago A generic decision procedure for linear rea arithmetic and normed vector spaces
2009-02-06 ago session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there