NEWS

--- a/NEWS	Mon Jan 23 14:34:07 2023 +0100
+++ b/NEWS	Mon Jan 23 14:40:23 2023 +0100
@@ -208,6 +208,13 @@
       totalp_on_multp
       wfP_subset_mset[simp]
 
+* Theory "HOL-Library.Multiset_Order":
+  - Added lemmas.
+      totalp_multpDM
+      totalp_multpHO
+      totalp_on_multpDM
+      totalp_on_multpHO
+
 * Mirabelle:
   - Added session to output directory structure. Minor INCOMPATIBILITY.