NEWS
changeset 73052 c03a148110cc
parent 73051 6ba08ec184a1
child 73078 824815ec52aa
--- a/NEWS	Mon Jan 04 21:25:40 2021 +0100
+++ b/NEWS	Tue Jan 05 03:35:46 2021 +0100
@@ -169,7 +169,8 @@
 division, instantiated for type int.
 
 * Theory "Multiset": removed misleading notation \<Union># for sum_mset;
-replaced with \<Sum>\<^sub>#.
+replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also 
+exists now.
 
 * Self-contained library theory "Word" taken over from former session
 "HOL-Word".