diff -r 66addfbb0923 -r 6714991edf8b NEWS
--- a/NEWS	Tue Dec 06 08:43:43 2022 +0100
+++ b/NEWS	Tue Dec 06 08:50:57 2022 +0100
@@ -31,8 +31,8 @@
     explicitly provided for backward compatibility but their usage is
     discouraged. Minor INCOMPATIBILITY.
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
-      preorder.irreflp_greater[simp] ~> irreflp_on_greater[simp]
-      preorder.irreflp_less[simp] ~> irreflp_on_less[simp]
+      preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
+      preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
       reflp_equality[simp] ~> reflp_on_equality[simp]
       total_on_singleton
   - Added lemmas.
@@ -40,10 +40,12 @@
       antisymp_if_asymp
       asym_if_irrefl_and_trans
       asymp_if_irreflp_and_transp
+      irreflD
       irrefl_onD
       irrefl_onI
       irrefl_on_converse[simp]
       irrefl_on_subset
+      irreflpD
       irreflp_onD
       irreflp_onI
       irreflp_on_converse[simp]