NEWS

--- a/NEWS	Tue Apr 02 11:41:50 2013 +0200
+++ b/NEWS	Tue Apr 02 16:29:40 2013 +0200
@@ -43,6 +43,8 @@
 
 *** HOL ***
 
+* Notation "{p:A. P}" now allows tuple patterns as well.
+
 * Revised devices for recursive definitions over finite sets:
   - Only one fundamental fold combinator on finite set remains:
     Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b