# HG changeset patch
# User paulson
# Date 965993200 -7200
# Node ID 9e66e8ed82375a443b85b07940398df2ee777272
# Parent  3df14e0a3a5189264d5f4d706221d4ea2a358262
ZF arith

diff -r 3df14e0a3a51 -r 9e66e8ed8237 NEWS
--- a/NEWS	Fri Aug 11 10:34:02 2000 +0200
+++ b/NEWS	Fri Aug 11 13:26:40 2000 +0200
@@ -269,16 +269,18 @@
 
 *** ZF ***
 
-* simplification automatically cancels common terms in arithmetic expressions over nat;
+* simplification automatically cancels common terms in arithmetic expressions
+over nat and int;
 
 * new treatment of nat to minimize type-checking: all operators coerce their 
 operands to a natural number using the function natify, making the algebraic
 laws unconditional;
 
-* as above, for int;
+* as above, for int: operators coerce their operands to an integer using the
+function intify;
 
 * the integer library now contains many of the usual laws for the orderings, 
-including $<=; 
+including $<=, and monotonicity laws for $+ and $*; 
 
 
 *** FOL & ZF ***