changeset 5541 | f8fb27db4bcd |
parent 5526 | e7617b57a3e6 |
child 5572 | 53c6ea1e6d94 |
--- a/NEWS Wed Sep 23 10:25:37 1998 +0200 +++ b/NEWS Wed Sep 23 10:56:08 1998 +0200 @@ -22,6 +22,10 @@ * HOL: unary - is now overloaded (new type constraints may be required); +* HOL and ZF: unary minus for integers is now #- instead of #~. In ZF, + expressions such as n#-1 must be changed to n#- 1, since #-1 is now taken + as an integer constant. + * Pure: ML function 'theory_of' replaced by 'theory';