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