NEWS
changeset 76495 a718547c3493
parent 76478 d84568379f3f
child 76496 855b5f0456d8
--- a/NEWS	Tue Nov 08 08:41:48 2022 +0100
+++ b/NEWS	Wed Nov 09 16:45:12 2022 +0100
@@ -47,6 +47,10 @@
       preorder.reflp_le[simp]
       totalp_on_singleton[simp]
 
+* Theory "HOL.Transitive_Closure":
+  - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp.
+    Minor INCOMPATIBILITY.
+
 * Theory "HOL.Wellfounded":
   - Added lemmas.
       wfP_if_convertible_to_nat