--- 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.