2010-03-01 ago replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-08 ago separate library theory for type classes combining lattices with various algebraic structures
2010-02-05 ago more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-11 ago Matrices form a semiring with 0
2009-11-13 ago renamed lemmas "anti_sym" -> "antisym"
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-09-02 ago reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
2009-08-28 ago tuned proofs
2009-01-31 ago added some simp rules
2009-01-28 ago Replaced group_ and ring_simps by algebra_simps;
2008-10-17 ago reactivated HOL-Matrix;
2008-10-10 ago `code func` now just `code`
2008-07-18 ago more class instantiations
2008-07-14 ago tuned
2008-07-04 ago added marginal setup for code generation
2008-01-02 ago removed some legacy instantiations
2007-11-29 ago instance command as rudimentary class target
2007-11-06 ago renamed lordered_*_* to lordered_*_add_*; further localization
2007-07-20 ago split class abs from class minus
2007-06-23 ago tuned and renamed group_eq_simps and ring_eq_simps
2007-03-16 ago adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
2007-03-09 ago stepping towards uniform lattice theory development in HOL
2006-11-12 ago started reorgnization of lattice theories
2006-09-20 ago renamed axclass_xxxx axclasses;
2005-10-19 ago isatool fixheaders;
2005-07-07 ago linear arithmetic now takes "&" in assumptions apart.
2005-02-01 ago the new subst tactic, by Lucas Dixon
2004-09-03 ago Matrix theory, linear programming
2004-06-14 ago Further development of matrix theory
2004-05-11 ago changes made due to new Ring_and_Field theory
2004-05-10 ago preparation for integration with new Ring_and_Field.thy
2004-05-01 ago tuned instance statements;
2004-04-23 ago proper document setup;
2004-04-16 ago first version of matrices for HOL/Isabelle