--- a/NEWS Sun May 07 14:52:53 2023 +0100
+++ b/NEWS Mon May 08 11:16:45 2023 +0200
@@ -247,6 +247,7 @@
multpDM_mono_strong
multpDM_plus_plusI[simp]
multpHO_double_double[simp]
+ multpHO_implies_one_step_strong
multpHO_mono_strong
multpHO_plus_plus[simp]
multpHO_repeat_mset_repeat_mset[simp]