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