Mon, 01 Jan 2001 11:50:31 +0100 |
paulson |
Hyperreal
|
changeset |
files
|
Sun, 31 Dec 2000 15:12:27 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
changeset |
files
|
Sat, 30 Dec 2000 22:19:30 +0100 |
paulson |
now #16*(x+y) distributes for nat just as for other numeric types
|
changeset |
files
|
Sat, 30 Dec 2000 22:17:34 +0100 |
paulson |
a generic ordering theorem used in Real
|
changeset |
files
|
Sat, 30 Dec 2000 22:13:18 +0100 |
paulson |
tidying, and separation of HOL-Hyperreal from HOL-Real
|
changeset |
files
|
Sat, 30 Dec 2000 22:03:47 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
changeset |
files
|
Sat, 30 Dec 2000 22:03:46 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
changeset |
files
|
Fri, 29 Dec 2000 19:46:00 +0100 |
wenzelm |
recover: ignore result;
|
changeset |
files
|
Fri, 29 Dec 2000 19:45:33 +0100 |
wenzelm |
recover: malformed result;
|
changeset |
files
|
Fri, 29 Dec 2000 19:45:01 +0100 |
wenzelm |
scan: malformed result;
|
changeset |
files
|
Fri, 29 Dec 2000 19:44:13 +0100 |
wenzelm |
recover: result;
|
changeset |
files
|
Fri, 29 Dec 2000 19:43:52 +0100 |
wenzelm |
proper error msg;
|
changeset |
files
|
Wed, 27 Dec 2000 18:27:49 +0100 |
wenzelm |
'erule' etc.: assm arg;
|
changeset |
files
|
Wed, 27 Dec 2000 18:27:19 +0100 |
wenzelm |
Method.erule 0;
|
changeset |
files
|