src/HOL/Matrix/SparseMatrix.thy
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Fri, 17 Oct 2008 10:39:39 +0200 wenzelm reactivated HOL-Matrix;
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Fri, 18 Jul 2008 18:25:57 +0200 haftmann more class instantiations
Fri, 04 Jul 2008 07:39:01 +0200 haftmann added marginal setup for code generation
Mon, 17 Mar 2008 18:37:00 +0100 wenzelm removed duplicate lemmas;
Tue, 06 Nov 2007 08:47:25 +0100 haftmann renamed lordered_*_* to lordered_*_add_*; further localization
Thu, 02 Aug 2007 12:06:27 +0200 wenzelm turned simp_depth_limit into configuration option;
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Fri, 16 Mar 2007 21:32:08 +0100 haftmann adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
Wed, 30 Aug 2006 03:19:08 +0200 webertj lin_arith_prover: splitting reverted because of performance loss
Wed, 02 Aug 2006 18:19:48 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Mon, 10 Apr 2006 16:00:34 +0200 obua Moved stuff from Ring_and_Field to Matrix
Mon, 20 Jun 2005 22:14:01 +0200 wenzelm proper header;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Mon, 23 May 2005 11:06:41 +0200 nipkow simplifier trace info; Suc-intervals
Mon, 07 Mar 2005 18:19:55 +0100 obua Cleaning up HOL/Matrix
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Mon, 11 Oct 2004 07:42:22 +0200 nipkow Proofs needed to be updated because induction now preserves name of
Fri, 10 Sep 2004 20:04:14 +0200 nipkow Added antisymmetry simproc
Fri, 03 Sep 2004 17:10:36 +0200 obua Matrix theory, linear programming
Tue, 29 Jun 2004 10:07:56 +0200 obua support for sparse matrices
less more (0) tip