author | nipkow |
Wed, 19 Sep 2007 15:26:58 +0200 | |
changeset 24649 | f7b68d12a91e |
parent 24648 | 1e8053a6d725 |
child 24650 | e2930fa53538 |
--- 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.