real numerals;
authorwenzelm
Sat, 21 Aug 1999 16:59:03 +0200
changeset 7313 300487ddfba9
parent 7312 523fb2832b30
child 7314 d3968533692c
real numerals;
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;