--- a/NEWS Sun Feb 04 23:05:35 2024 +0100
+++ b/NEWS Mon Feb 05 10:06:34 2024 +0100
@@ -40,6 +40,11 @@
* Lemma even_succ_div_2 renamed to even_half_succ_eq. Minor INCOMPATIBILITY.
+* Theory "HOL-Library.Multiset":
+ - Added lemmas.
+ trans_on_mult
+ transp_on_multp
+
*** ML ***