# HG changeset patch
# User desharna
# Date 1668004723 -3600
# Node ID 11077c158b37fa6e38a8321c0b50074802d59fb7
# Parent  ebcfaddd3cb616c037c0b2b6a270218076b53ddd
added lemma transp_reflclp[simp]

diff -r ebcfaddd3cb6 -r 11077c158b37 NEWS
--- a/NEWS	Wed Nov 09 15:37:21 2022 +0100
+++ b/NEWS	Wed Nov 09 15:38:43 2022 +0100
@@ -53,6 +53,7 @@
   - Added lemmas.
       reflclp_ident_if_reflp[simp]
       reflp_on_reflclp[simp]
+      transp_reflclp[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
diff -r ebcfaddd3cb6 -r 11077c158b37 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Nov 09 15:37:21 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 09 15:38:43 2022 +0100
@@ -79,6 +79,9 @@
 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 reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
   by blast