# HG changeset patch
# User paulson
# Date 959260257 -7200
# Node ID 00f18476ac15b3089e19f2c75a3846284b03ec64
# Parent  916966f689076d3a8514a55fd9741d4b5cc06b5a
overloading of 0

diff -r 916966f68907 -r 00f18476ac15 NEWS
--- a/NEWS	Wed May 24 19:09:50 2000 +0200
+++ b/NEWS	Thu May 25 15:10:57 2000 +0200
@@ -14,6 +14,9 @@
   Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
 
+* HOL: 0 is now overloaded, so the type constraint ::nat may sometimes be
+needed;
+
 * HOL: the constant for f``x is now "image" rather than "op ``";
 
 * HOL: the cartesian product is now "<*>" instead of "Times"; the
@@ -136,6 +139,12 @@
 
 * HOL/Real: "rabs" replaced by overloaded "abs" function;
 
+* HOL: 0 is now overloaded over the new sort "zero", allowing its use with
+other numeric types and also as the identity of groups, rings, etc.;
+
+* HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity.
+Types nat and int belong to this axclass;
+
 * greatly improved simplification involving numerals of type nat & int, e.g.
    (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
    i*j + k + j*#3*i     simplifies to  #4*(i*j) + k