# HG changeset patch
# User nipkow
# Date 1739033149 -3600
# Node ID ab0030db61fdf3e7dfdd7bfb3cb990a7e9011250
# Parent  eebb8270b3cc1ca36d71b54dac7813e711d9d98c
added lemma

diff -r eebb8270b3cc -r ab0030db61fd src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Feb 08 11:18:30 2025 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sat Feb 08 17:45:49 2025 +0100
@@ -676,6 +676,9 @@
 lemma rtrancl_empty [simp]: "{}\<^sup>* = Id"
   by (rule subst [OF reflcl_trancl]) simp
 
+lemma rtrancl__Id[simp]: "Id\<^sup>* = Id"
+using rtrancl_empty rtrancl_idemp[of "{}"] by (simp)
+
 lemma rtranclpD: "R\<^sup>*\<^sup>* a b \<Longrightarrow> a = b \<or> a \<noteq> b \<and> R\<^sup>+\<^sup>+ a b"
   by (force simp: reflclp_tranclp [symmetric] simp del: reflclp_tranclp)