| Thu, 01 Jan 2004 10:06:32 +0100 |
paulson |
tweaking of lemmas in RealDef, RealOrd
|
file |
diff |
annotate
|
| Thu, 25 Dec 2003 22:48:32 +0100 |
paulson |
re-organized some hyperreal and real lemmas
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 14:46:08 +0100 |
paulson |
new theorems
|
file |
diff |
annotate
|
| Mon, 02 Sep 2002 12:25:19 +0200 |
paulson |
Added missing rewrite rule and some arith examples
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Wed, 12 Dec 2001 19:22:21 +0100 |
nipkow |
new rewrite rules for use by arith_tac to take care of uminus.
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 17:55:24 +0100 |
paulson |
Numerals and simprocs for types real and hypreal. The abstract
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Tue, 02 Jan 2001 10:35:33 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 01 Jan 2001 11:52:04 +0100 |
paulson |
minor tidying of simprocs
|
file |
diff |
annotate
|
| Thu, 21 Dec 2000 18:57:12 +0100 |
nipkow |
rational linear arithmetic
|
file |
diff |
annotate
|