overloading of 0
authorpaulson
Thu May 25 15:10:57 2000 +0200 (2000-05-25)
changeset 896700f18476ac15
parent 8966 916966f68907
child 8968 2e88a982f96b
overloading of 0
NEWS
     1.1 --- a/NEWS	Wed May 24 19:09:50 2000 +0200
     1.2 +++ b/NEWS	Thu May 25 15:10:57 2000 +0200
     1.3 @@ -14,6 +14,9 @@
     1.4    Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
     1.5    Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
     1.6  
     1.7 +* HOL: 0 is now overloaded, so the type constraint ::nat may sometimes be
     1.8 +needed;
     1.9 +
    1.10  * HOL: the constant for f``x is now "image" rather than "op ``";
    1.11  
    1.12  * HOL: the cartesian product is now "<*>" instead of "Times"; the
    1.13 @@ -136,6 +139,12 @@
    1.14  
    1.15  * HOL/Real: "rabs" replaced by overloaded "abs" function;
    1.16  
    1.17 +* HOL: 0 is now overloaded over the new sort "zero", allowing its use with
    1.18 +other numeric types and also as the identity of groups, rings, etc.;
    1.19 +
    1.20 +* HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity.
    1.21 +Types nat and int belong to this axclass;
    1.22 +
    1.23  * greatly improved simplification involving numerals of type nat & int, e.g.
    1.24     (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
    1.25     i*j + k + j*#3*i     simplifies to  #4*(i*j) + k