diff -r 39f8051f71d4 -r 1c358879bfd3 NEWS
--- a/NEWS	Sun Jan 22 23:29:34 2023 +0100
+++ b/NEWS	Mon Jan 23 13:31:07 2023 +0100
@@ -66,6 +66,8 @@
     be abbreviations. Lemmas trans_def and transp_def are explicitly provided
     for backward compatibility but their usage is discouraged.
     Minor INCOMPATIBILITY.
+  - Renamed wrongly named lemma totalp_on_refl_on_eq to totalp_on_total_on_eq.
+    Minor INCOMPATIBILITY.
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       antisym_converse[simp] ~> antisym_on_converse[simp]
       order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]