--- a/NEWS Sun Jun 03 12:58:28 2007 +0200
+++ b/NEWS Sun Jun 03 13:19:03 2007 +0200
@@ -560,8 +560,9 @@
* new function listsum :: 'a list => 'a for arbitrary monoids.
Special syntax: "SUM x <- xs. f x" (and latex variants)
-* Library/List_Comprehension.thy provides Haskell-like input syntax for list
- comprehensions.
+* new (input only) syntax for Haskell-like list comprehension, eg
+ [(x,y). x <- xs, y <- ys, x ~= y]
+ For details see List.thy.
* Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
when generating code.