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