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