NEWS
changeset 76522 3fc92362fbb5
parent 76521 15f868460de9
child 76559 4352d0ff165a
--- a/NEWS	Mon Nov 21 13:48:58 2022 +0100
+++ b/NEWS	Mon Nov 21 13:53:04 2022 +0100
@@ -26,8 +26,9 @@
     Minor INCOMPATIBILITY.
 
 * Theory "HOL.Relation":
-  - Strengthened lemmas. Minor INCOMPATIBILITY.
+  - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       total_on_singleton
+      reflp_equality[simp] ~> reflp_on_equality[simp]
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp