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