# HG changeset patch
# User nipkow
# Date 1739033170 -3600
# Node ID 0c54f3c06174622549f5266c456a4fcc368e273c
# Parent  bb6a3b379f6a23875cb85f48bc4a7cc4339f86ac# Parent  ab0030db61fdf3e7dfdd7bfb3cb990a7e9011250
merged

diff -r bb6a3b379f6a -r 0c54f3c06174 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Feb 08 17:44:04 2025 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sat Feb 08 17:46:10 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)