NEWS
changeset 68125 2e5b737810a6
parent 68116 ac82ee617a75
child 68157 057d5b4ce47e
     1.1 --- a/NEWS	Tue May 08 21:03:06 2018 +0100
     1.2 +++ b/NEWS	Wed May 09 07:48:54 2018 +0200
     1.3 @@ -296,7 +296,6 @@
     1.4    - span_eq ~> span_eq_iff
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -
     1.8  * HOL-Algebra: renamed (^) to [^]
     1.9  
    1.10  * Session HOL-Analysis: Moebius functions, the Riemann mapping
    1.11 @@ -306,6 +305,9 @@
    1.12  * Class linordered_semiring_1 covers zero_less_one also, ruling out
    1.13  pathologic instances. Minor INCOMPATIBILITY.
    1.14  
    1.15 +* Theory List: functions "sorted_wrt" and "sorted" now compare every
    1.16 +  element in a list to all following elements, not just the next one.
    1.17 +
    1.18  * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
    1.19  
    1.20  * Predicate coprime is now a real definition, not a mere