# HG changeset patch
# User desharna
# Date 1668008712 -3600
# Node ID a718547c34933a8e93d13f8737b3105b8bf4dbd3
# Parent  3d281371b2137ddb947a1cef789693b041201f34
strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp

diff -r 3d281371b213 -r a718547c3493 NEWS
--- 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
diff -r 3d281371b213 -r a718547c3493 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Nov 08 08:41:48 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 09 16:45:12 2022 +0100
@@ -762,8 +762,9 @@
 lemma symclp_idem [simp]: "symclp (symclp r) = symclp r"
   by(simp add: symclp_pointfree sup_commute converse_join)
 
-lemma reflp_rtranclp [simp]: "reflp R\<^sup>*\<^sup>*"
-  using refl_rtrancl[to_pred, of R] reflp_refl_eq[of "{(x, y). R\<^sup>*\<^sup>* x y}"] by simp
+lemma reflp_on_rtranclp [simp]: "reflp_on A R\<^sup>*\<^sup>*"
+  by (simp add: reflp_on_def)
+
 
 subsection \<open>The power operation on relations\<close>