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

author | ballarin |

Sat, 10 Feb 2001 08:48:10 +0100 | |

changeset 11091 | 45ffef3d3e75 |

parent 11090 | 3041d0347d26 |

child 11092 | 69c1abb9a129 |

Updates to HOL/Algebra:
- axclasses consolidated (lemma one_not_zero)
- summation operator SUM removed, now uses setsum
Use of setsum made it necessary to relax sort constraint in its definition
to {zero, plus}.

--- a/NEWS Fri Feb 09 23:48:50 2001 +0100 +++ b/NEWS Sat Feb 10 08:48:10 2001 +0100 @@ -7,6 +7,12 @@ *** Overview of INCOMPATIBILITIES *** +* HOL/Algebra: special summation operator SUM no longer exists, it has +been replaced by setsum; infix 'assoc' now has priority 50 (like 'dvd'); + +* HOL/Algebra: axiom 'one_not_zero' has been moved from axclass 'ring' +to 'domain', this makes the theory consistent with mathematical literature; + * HOL: inductive package no longer splits induction rule aggressively, but only as far as specified by the introductions given; the old format may recovered via ML function complete_split_rule or attribute