diff -r 4dd01eb1e0cb -r d10a49b7b620 NEWS
--- a/NEWS	Mon Mar 17 09:00:40 2025 +0100
+++ b/NEWS	Mon Mar 17 09:12:18 2025 +0100
@@ -40,16 +40,24 @@
       irreflp_on_bot[simp]
       left_unique_bot[simp]
       left_unique_iff_Uniq
+      refl_on_top[simp]
       reflp_on_refl_on_eq[pred_set_conv]
+      reflp_on_top[simp]
       sym_on_bot[simp]
+      sym_on_top[simp]
       symp_on_bot[simp]
       symp_on_equality[simp]
+      symp_on_top[simp]
+      total_on_top[simp]
       totalp_on_mono[mono]
       totalp_on_mono_strong
       totalp_on_mono_stronger
       totalp_on_mono_stronger_alt
+      totalp_on_top[simp]
       trans_on_bot[simp]
+      trans_on_top[simp]
       transp_on_bot[simp]
+      transp_on_top[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.