| changeset 7313 | 300487ddfba9 |
| parent 7300 | 8439bf404c28 |
| child 7320 | e89fd7d0a624 |
--- 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;