diff -r 0fb476ff855c -r 831c864cc56e NEWS
--- a/NEWS	Sun Dec 31 15:12:27 2000 +0100
+++ b/NEWS	Mon Jan 01 11:50:31 2001 +0100
@@ -78,6 +78,10 @@
 * HOL/typedef: simplified package, provide more useful rules (see also
 HOL/subset.thy);
 
+* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and 
+Fleuriot's mechanization of analysis;
+
+* HOL-Real, HOL-Hyperreals: improved arithmetic simplification;
 
 *** CTT ***