author | ballarin |

Sat Feb 10 08:48:10 2001 +0100 (2001-02-10) | |

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

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

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