author | paulson |

Thu May 25 15:10:57 2000 +0200 (2000-05-25) | |

changeset 8967 | 00f18476ac15 |

parent 8966 | 916966f68907 |

child 8968 | 2e88a982f96b |

overloading of 0

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