src/HOL/Matrix/SparseMatrix.thy
2010-08-11 wenzelm 2010-08-11 modernized some specifications;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-09-02 wenzelm 2009-09-02 reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
2009-06-27 nipkow 2009-06-27 removed old primrecs
2009-06-27 nipkow 2009-06-27 replaced recdefs by funs
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-04 haftmann 2008-07-04 added marginal setup for code generation
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2007-11-06 haftmann 2007-11-06 renamed lordered_*_* to lordered_*_add_*; further localization
2007-08-02 wenzelm 2007-08-02 turned simp_depth_limit into configuration option;
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
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-08-02 webertj 2006-08-02 lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-04-10 obua 2006-04-10 Moved stuff from Ring_and_Field to Matrix
2005-06-20 wenzelm 2005-06-20 proper header;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-23 nipkow 2005-05-23 simplifier trace info; Suc-intervals
2005-03-07 obua 2005-03-07 Cleaning up HOL/Matrix
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-09-10 nipkow 2004-09-10 Added antisymmetry simproc
2004-09-03 obua 2004-09-03 Matrix theory, linear programming
2004-06-29 obua 2004-06-29 support for sparse matrices