# HG changeset patch
# User nipkow
# Date 1108576849 -3600
# Node ID fad04f5f822f6206e3d3ba90616b6faf226a3897
# Parent  accd51fdae3c27be3c13f3152152419299a837ae
*** empty log message ***

diff -r accd51fdae3c -r fad04f5f822f NEWS
--- a/NEWS	Tue Feb 15 16:56:15 2005 +0100
+++ b/NEWS	Wed Feb 16 19:00:49 2005 +0100
@@ -239,6 +239,9 @@
   Similarly for all quantifiers: "ALL x > y" etc.
   The x-symbol for >= is \<ge>.
 
+* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}"
+           (and similarly for "\<in>" instead of ":")
+
 * HOL/SetInterval: The syntax for open intervals has changed:
 
   Old         New