--- a/NEWS Mon Jan 23 14:40:23 2023 +0100 +++ b/NEWS Mon Jan 23 15:11:50 2023 +0100 @@ -210,6 +210,7 @@ * Theory "HOL-Library.Multiset_Order": - Added lemmas. + irreflp_on_multpHO[simp] totalp_multpDM totalp_multpHO totalp_on_multpDM