--- a/NEWS Mon Nov 19 23:37:01 2001 +0100
+++ b/NEWS Tue Nov 20 10:48:38 2001 +0100
@@ -418,8 +418,9 @@
* HOL: improved concrete syntax for strings (e.g. allows translation
rules with string literals);
-* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals
-and Fleuriot's mechanization of analysis;
+* HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals
+ and Fleuriot's mechanization of analysis, including the transcendental
+ functions for the reals;
* HOL/Real, HOL/Hyperreal: improved arithmetic simplification;