--- 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":
--- a/src/HOL/Transitive_Closure.thy Wed Nov 09 16:39:45 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Nov 09 15:37:21 2022 +0100
@@ -82,6 +82,9 @@
lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
by blast
+lemma reflclp_ident_if_reflp[simp]: "reflp R \<Longrightarrow> R\<^sup>=\<^sup>= = R"
+ by (auto dest: reflpD)
+
subsection \<open>Reflexive-transitive closure\<close>