Tue, 02 Jan 2001 11:03:37 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Tue, 02 Jan 2001 10:35:33 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Tue, 02 Jan 2001 10:27:10 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Mon, 01 Jan 2001 11:52:04 +0100 |
paulson |
minor tidying of simprocs
|
changeset |
files
|
Mon, 01 Jan 2001 11:51:20 +0100 |
paulson |
put in some missing Hyperreal files
|
changeset |
files
|
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
|