*** empty log message ***
authornipkow
Wed, 16 Feb 2005 19:00:49 +0100
changeset 15534 fad04f5f822f
parent 15533 accd51fdae3c
child 15535 a0cf3a19ee36
*** empty log message ***
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