# HG changeset patch # User wenzelm # Date 1364912980 -7200 # Node ID 4f25e800f5203a3f53fa351dcc3d493a3f93f81e # Parent 8e9746e584c9440a9d2a1c3cbd1ac166ebd255f6 NEWS for 635562bc14ef; diff -r 8e9746e584c9 -r 4f25e800f520 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