# HG changeset patch
# User wenzelm
# Date 935247543 -7200
# Node ID 300487ddfba98fc6d8f92025b5b27696ce929355
# Parent  523fb2832b30624bbdb9d8091a0a0401fc42a062
real numerals;

diff -r 523fb2832b30 -r 300487ddfba9 NEWS
--- a/NEWS	Sat Aug 21 16:54:09 1999 +0200
+++ b/NEWS	Sat Aug 21 16:59:03 1999 +0200
@@ -124,7 +124,7 @@
 int(m) < int(n)'.
 
 * HOL/Numeral provides a generic theory of numerals (encoded
-efficiently as bit strings); setup for types nat and int is in place;
+efficiently as bit strings); setup for types nat/int/real is in place;
 INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than
 int, existing theories and proof scripts may require a few additional
 type constraints;