| changeset 10756 | 831c864cc56e |
| parent 10726 | e12b81140945 |
| child 10770 | 4858ad0b8f38 |
--- a/NEWS Sun Dec 31 15:12:27 2000 +0100 +++ b/NEWS Mon Jan 01 11:50:31 2001 +0100 @@ -78,6 +78,10 @@ * HOL/typedef: simplified package, provide more useful rules (see also HOL/subset.thy); +* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and +Fleuriot's mechanization of analysis; + +* HOL-Real, HOL-Hyperreals: improved arithmetic simplification; *** CTT ***