| Fri, 05 Jan 2001 18:48:18 +0100 |
nipkow |
^^ -> ```
|
file |
diff |
annotate
|
| Sat, 30 Dec 2000 22:13:18 +0100 |
paulson |
tidying, and separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|
| Wed, 20 Dec 2000 12:15:52 +0100 |
paulson |
further tidying
|
file |
diff |
annotate
|
| Tue, 12 Dec 2000 12:01:19 +0100 |
paulson |
first stage in tidying up Real and Hyperreal.
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 12:34:12 +0100 |
bauerg |
converted rinv to inverse;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2000 10:23:16 +0200 |
paulson |
restoration of "equalityI"; renaming of contrapos rules
|
file |
diff |
annotate
|
| Thu, 21 Sep 2000 12:11:38 +0200 |
fleuriot |
Updated Files with new theorems
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 12:39:57 +0200 |
paulson |
renamed (most of...) the select rules
|
file |
diff |
annotate
|
| Mon, 24 Jul 2000 23:51:46 +0200 |
wenzelm |
avoid referencing thy value;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2000 12:33:19 +0200 |
paulson |
changed / to // for quotienting; general tidying
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:57:34 +0200 |
wenzelm |
use pair_tac;
|
file |
diff |
annotate
|
| Thu, 06 Jul 2000 15:01:52 +0200 |
paulson |
removal of batch style, and tidying
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:50:27 +0200 |
paulson |
got rid of weak elim rule
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Wed, 07 Jun 2000 12:14:18 +0200 |
paulson |
First round of changes, towards installation of simprocs
|
file |
diff |
annotate
|
| Tue, 23 Nov 1999 11:19:39 +0100 |
paulson |
distributive laws for * over -
|
file |
diff |
annotate
|
| Tue, 07 Sep 1999 10:40:58 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 21:25:55 +0200 |
wenzelm |
bind_thms;
|
file |
diff |
annotate
|
| Thu, 19 Aug 1999 18:36:41 +0200 |
paulson |
real literals using binary arithmetic
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 18:41:32 +0200 |
paulson |
inserted Id: lines
|
file |
diff |
annotate
|
| Thu, 29 Jul 1999 12:44:57 +0200 |
paulson |
added parentheses to cope with a possible reduction of the precedence of unary
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 17:29:12 +0200 |
paulson |
heavily revised by Jacques: coercions have alphabetic names;
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:18:01 +0200 |
paulson |
Revised version with Abelian group simprocs
|
file |
diff |
annotate
|