| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 18:19:48 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 16:00:34 +0200 |
obua |
Moved stuff from Ring_and_Field to Matrix
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:01 +0200 |
wenzelm |
proper header;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 23 May 2005 11:06:41 +0200 |
nipkow |
simplifier trace info; Suc-intervals
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 18:19:55 +0100 |
obua |
Cleaning up HOL/Matrix
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Mon, 11 Oct 2004 07:42:22 +0200 |
nipkow |
Proofs needed to be updated because induction now preserves name of
|
file |
diff |
annotate
|
| Fri, 10 Sep 2004 20:04:14 +0200 |
nipkow |
Added antisymmetry simproc
|
file |
diff |
annotate
|
| Fri, 03 Sep 2004 17:10:36 +0200 |
obua |
Matrix theory, linear programming
|
file |
diff |
annotate
|
| Tue, 29 Jun 2004 10:07:56 +0200 |
obua |
support for sparse matrices
|
file |
diff |
annotate
|