--- 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
--- 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>