unary minus
authorpaulson
Wed Sep 23 10:56:08 1998 +0200 (1998-09-23)
changeset 5541f8fb27db4bcd
parent 5540 0f16c3b66ab4
child 5542 f0c303f53730
unary minus
NEWS
     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