# HG changeset patch
# User paulson
# Date 1006249718 -3600
# Node ID 3dd9aae402bbe0263cec0d61842ecd9208a90ff8
# Parent  179f142ffb03e5791dacb3ce350c401781d428e5
Hyperreal

diff -r 179f142ffb03 -r 3dd9aae402bb NEWS
--- 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;