NEWS
changeset 9577 9e66e8ed8237
parent 9542 fa19ffdbe1de
child 9612 e6ba17cd012e
     1.1 --- a/NEWS	Fri Aug 11 10:34:02 2000 +0200
     1.2 +++ b/NEWS	Fri Aug 11 13:26:40 2000 +0200
     1.3 @@ -269,16 +269,18 @@
     1.4  
     1.5  *** ZF ***
     1.6  
     1.7 -* simplification automatically cancels common terms in arithmetic expressions over nat;
     1.8 +* simplification automatically cancels common terms in arithmetic expressions
     1.9 +over nat and int;
    1.10  
    1.11  * new treatment of nat to minimize type-checking: all operators coerce their 
    1.12  operands to a natural number using the function natify, making the algebraic
    1.13  laws unconditional;
    1.14  
    1.15 -* as above, for int;
    1.16 +* as above, for int: operators coerce their operands to an integer using the
    1.17 +function intify;
    1.18  
    1.19  * the integer library now contains many of the usual laws for the orderings, 
    1.20 -including $<=; 
    1.21 +including $<=, and monotonicity laws for $+ and $*; 
    1.22  
    1.23  
    1.24  *** FOL & ZF ***