--- 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)