NEWS
changeset 12245 3dd9aae402bb
parent 12210 2f510d8d8291
child 12253 1886dc96b7e9
     1.1 --- a/NEWS	Mon Nov 19 23:37:01 2001 +0100
     1.2 +++ b/NEWS	Tue Nov 20 10:48:38 2001 +0100
     1.3 @@ -418,8 +418,9 @@
     1.4  * HOL: improved concrete syntax for strings (e.g. allows translation
     1.5  rules with string literals);
     1.6  
     1.7 -* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals
     1.8 -and Fleuriot's mechanization of analysis;
     1.9 +* HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals
    1.10 + and Fleuriot's mechanization of analysis, including the transcendental
    1.11 + functions for the reals;
    1.12  
    1.13  * HOL/Real, HOL/Hyperreal: improved arithmetic simplification;
    1.14