--- 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