| changeset 66937 | a1a4a5e2933a |
| parent 66909 | 9eaa9504991b |
| child 66949 | 6c5e4ac0398b |
--- a/NEWS Mon Oct 30 13:18:41 2017 +0000 +++ b/NEWS Mon Oct 30 13:18:44 2017 +0000 @@ -63,6 +63,9 @@ * Session HOL-Analysis: Moebius functions and the Riemann mapping theorem. +* Class linordered_semiring_1 covers zero_less_one also, ruling out +pathologic instances. Minor INCOMPATIBILITY. + *** System ***