# HG changeset patch
# User nipkow
# Date 1196433614 -3600
# Node ID 00b59b9c7c833bdfe6f500a9450d068c8a9e4967
# Parent  d13468d4013149de829a45b78e2e8fef0b34068b
*** empty log message ***

diff -r d13468d40131 -r 00b59b9c7c83 NEWS
--- a/NEWS	Fri Nov 30 11:51:22 2007 +0100
+++ b/NEWS	Fri Nov 30 15:40:14 2007 +0100
@@ -14,6 +14,8 @@
 
 *** HOL ***
 
+* Library/Multiset: {#a, b, c#} is new short syntax for {#a#} + {#b#} + {#c#}.
+
 * Constant "card" now with authentic syntax.