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

author | krauss |

Tue, 07 Nov 2006 09:41:14 +0100 | |

changeset 21200 | 2f6e276bfb93 |

parent 21199 | 2d83f93c3580 |

child 21201 | 803bc7672d17 |

updated NEWS

--- a/NEWS Tue Nov 07 09:33:47 2006 +0100 +++ b/NEWS Tue Nov 07 09:41:14 2006 +0100 @@ -475,6 +475,18 @@ *** HOL *** +* axclass "semiring_0" now contains annihilation axioms +("x * 0 = 0","0 * x = 0"), which are required for a semiring. Richer +structures do not inherit from semiring_0 anymore, because this property +is a theorem there, not an axiom. +INCOMPATIBILITY: In instances of semiring_0, there is more to prove, but +this is mostly trivial. + +* axclass "recpower" was generalized to arbitrary monoids, not just +commutative semirings. +INCOMPATIBILITY: If you use recpower and need commutativity or a semiring +property, add the corresponding classes. + * Constant "List.list_all2" in List.thy now uses authentic syntax. INCOMPATIBILITY: translations containing list_all2 may go wrong. On Isar level, use abbreviations instead.