Hyperreal
authorpaulson
Tue Nov 20 10:48:38 2001 +0100 (2001-11-20)
changeset 122453dd9aae402bb
parent 12244 179f142ffb03
child 12246 fdb65a05fca8
Hyperreal
NEWS
     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