real numerals;
authorwenzelm
Sat Aug 21 16:59:03 1999 +0200 (1999-08-21)
changeset 7313300487ddfba9
parent 7312 523fb2832b30
child 7314 d3968533692c
real numerals;
NEWS
     1.1 --- a/NEWS	Sat Aug 21 16:54:09 1999 +0200
     1.2 +++ b/NEWS	Sat Aug 21 16:59:03 1999 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4  int(m) < int(n)'.
     1.5  
     1.6  * HOL/Numeral provides a generic theory of numerals (encoded
     1.7 -efficiently as bit strings); setup for types nat and int is in place;
     1.8 +efficiently as bit strings); setup for types nat/int/real is in place;
     1.9  INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than
    1.10  int, existing theories and proof scripts may require a few additional
    1.11  type constraints;