# HG changeset patch
# User nipkow
# Date 1181463822 -7200
# Node ID b785068bd5dc5b54f28562e7507a494f8a402caa
# Parent  292b1cbd05dcc8ec453339bf2bad2c50c759c751
*** empty log message ***

diff -r 292b1cbd05dc -r b785068bd5dc NEWS
--- 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.