--- a/NEWS Wed Nov 09 16:39:45 2022 +0100
+++ b/NEWS Wed Nov 09 15:37:21 2022 +0100
@@ -51,6 +51,7 @@
- Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp.
Minor INCOMPATIBILITY.
- Added lemmas.
+ reflclp_ident_if_reflp[simp]
reflp_on_reflclp[simp]
* Theory "HOL.Wellfounded":