# HG changeset patch
# User desharna
# Date 1671462357 -3600
# Node ID f70a7ff13b1051e5eab61fbac27934ba0e978e0a
# Parent  11a24dab1880f8d21377124e5128a754a8cc051f
strengthened and renamed transp_reflclp

diff -r 11a24dab1880 -r f70a7ff13b10 NEWS
--- a/NEWS	Mon Dec 19 16:00:49 2022 +0100
+++ b/NEWS	Mon Dec 19 16:05:57 2022 +0100
@@ -131,7 +131,7 @@
       antisymp_on_reflcp[simp]
       reflclp_ident_if_reflp[simp]
       reflp_on_reflclp[simp]
-      transp_reflclp[simp]
+      transp_on_reflclp[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
diff -r 11a24dab1880 -r f70a7ff13b10 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Dec 19 16:00:49 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Dec 19 16:05:57 2022 +0100
@@ -85,8 +85,8 @@
 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans (r\<^sup>=)"
   unfolding trans_def by blast
 
-lemma transp_reflclp[simp]: "transp R \<Longrightarrow> transp R\<^sup>=\<^sup>="
-  unfolding transp_def by blast
+lemma transp_on_reflclp[simp]: "transp_on A R \<Longrightarrow> transp_on A R\<^sup>=\<^sup>="
+  by (auto intro: transp_onI dest: transp_onD)
 
 lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
   by blast