NEWS
changeset 15534 fad04f5f822f
parent 15531 08c8dad8e399
child 15570 8d8c70b41bab
--- 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