--- a/NEWS Sat Jun 09 02:38:51 2007 +0200
+++ b/NEWS Sun Jun 10 10:23:42 2007 +0200
@@ -31,7 +31,7 @@
these tend to cause confusion about the actual goal (!) context being
used here, which is not necessarily the same as the_context().
-* Command 'find_theorems': support "*" wildcard in "name:" criterion.
+* Command 'find_theorems': supports "*" wildcard in "name:" criterion.
* Proof General interface: A search form for the "Find Theorems" command is
now available via C-c C-a C-f. The old minibuffer interface is available
@@ -574,6 +574,10 @@
[(x,y). x <- xs, y <- ys, x ~= y]
For details see List.thy.
+* The special syntax for function "filter" has changed from [x : xs. P] to
+ [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax,
+ and for uniformity. INCOMPATIBILITY
+
* Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
when generating code.