# HG changeset patch
# User paulson
# Date 906540968 -7200
# Node ID f8fb27db4bcd8c8a48ed1c833ab7aeac5fd48e15
# Parent  0f16c3b66ab4d479cf4edad7ab1096675f054616
unary minus

diff -r 0f16c3b66ab4 -r f8fb27db4bcd NEWS
--- 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';