src/HOL/Matrix/MatrixGeneral.thy
Thu, 29 Nov 2007 17:08:26 +0100 haftmann instance command as rudimentary class target
Wed, 13 Jun 2007 18:30:11 +0200 wenzelm tuned proofs: avoid implicit prems;
Mon, 11 Jun 2007 11:06:04 +0200 chaieb tuned Proof
Fri, 16 Mar 2007 21:32:14 +0100 haftmann tuned
Fri, 02 Feb 2007 15:47:58 +0100 nipkow a few additions and deletions
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)
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Thu, 28 Jul 2005 15:19:48 +0200 wenzelm fixed var index in tactic;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Thu, 21 Apr 2005 18:58:44 +0200 berghofe Modified variable index in proof (necessary due to changes in the kernel).
Mon, 07 Mar 2005 18:19:55 +0100 obua Cleaning up HOL/Matrix
Wed, 02 Feb 2005 18:06:25 +0100 paulson tidying of some subst/simplesubst proofs
Wed, 02 Feb 2005 10:16:33 +0100 nipkow Max_le -> Max_ge
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Thu, 09 Dec 2004 18:30:59 +0100 nipkow First step in reorganizing Finite_Set
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
Mon, 14 Jun 2004 14:20:55 +0200 obua Further development of matrix theory
Sat, 01 May 2004 22:01:57 +0200 wenzelm tuned instance statements;
Fri, 23 Apr 2004 20:49:26 +0200 wenzelm proper document setup;
Thu, 22 Apr 2004 12:18:23 +0200 wenzelm fixed constdefs typing;
Fri, 16 Apr 2004 18:30:51 +0200 obua first version of matrices for HOL/Isabelle
less more (0) tip