*** empty log message ***
authornipkow
Wed, 19 Sep 2007 15:26:58 +0200
changeset 24649 f7b68d12a91e
parent 24648 1e8053a6d725
child 24650 e2930fa53538
*** empty log message ***
NEWS
--- 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.