# HG changeset patch
# User desharna
# Date 1668008385 -3600
# Node ID 855b5f0456d8f2d7376e4faf88c6b5c1b691a5f7
# Parent  a718547c34933a8e93d13f8737b3105b8bf4dbd3
added lemma reflp_on_reflclp[simp]

diff -r a718547c3493 -r 855b5f0456d8 NEWS
--- a/NEWS	Wed Nov 09 16:45:12 2022 +0100
+++ b/NEWS	Wed Nov 09 16:39:45 2022 +0100
@@ -50,6 +50,8 @@
 * Theory "HOL.Transitive_Closure":
   - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp.
     Minor INCOMPATIBILITY.
+  - Added lemmas.
+      reflp_on_reflclp[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
diff -r a718547c3493 -r 855b5f0456d8 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Nov 09 16:45:12 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 09 16:39:45 2022 +0100
@@ -70,6 +70,9 @@
 lemma refl_reflcl[simp]: "refl (r\<^sup>=)"
   by (simp add: refl_on_def)
 
+lemma reflp_on_reflclp[simp]: "reflp_on A R\<^sup>=\<^sup>="
+  by (simp add: reflp_on_def)
+
 lemma antisym_reflcl[simp]: "antisym (r\<^sup>=) = antisym r"
   by (simp add: antisym_def)