# HG changeset patch
# User paulson
# Date 978346231 -3600
# Node ID 831c864cc56e53dee099903a92196f7d154b290f
# Parent  0fb476ff855c9ea8977cf3ed3f7ff01da0fbb611
Hyperreal

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 ***