| changeset 24649 | f7b68d12a91e |
| parent 24643 | d5e4b170d132 |
| child 24692 | a5d89a87e8e3 |
--- a/NEWS Wed Sep 19 13:59:13 2007 +0200 +++ b/NEWS Wed Sep 19 15:26:58 2007 +0200 @@ -737,6 +737,10 @@ [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax, and for uniformity. INCOMPATIBILITY +* [a..b] is now defined for arbitrary linear orders. + It used to be defined on nat only, as an abbreviation for [a..<Suc b] + INCOMPATIBILITY + * Lemma "set_take_whileD" renamed to "set_takeWhileD" * new functions sorted and sort in List.