NEWS
changeset 76496 855b5f0456d8
parent 76495 a718547c3493
child 76497 ebcfaddd3cb6
--- a/NEWS	Wed Nov 09 16:45:12 2022 +0100
+++ b/NEWS	Wed Nov 09 16:39:45 2022 +0100
@@ -50,6 +50,8 @@
 * Theory "HOL.Transitive_Closure":
   - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp.
     Minor INCOMPATIBILITY.
+  - Added lemmas.
+      reflp_on_reflclp[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.