diff -r f38693aad717 -r 090c6a98c704 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Jun 21 09:51:59 2005 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Jun 21 11:08:31 2005 +0200
@@ -384,6 +384,9 @@
 lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+"
   by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
 
+lemma rtrancl_eq_or_trancl:
+  "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)"
+  by (fast elim: trancl_into_rtrancl dest: rtranclD)
 
 text {* @{text Domain} and @{text Range} *}