summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 25 May 2000 15:10:57 +0200 | |

changeset 8967 | 00f18476ac15 |

parent 8966 | 916966f68907 |

child 8968 | 2e88a982f96b |

overloading of 0

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