
diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/Transitive_Closure.thy	Thu Dec 20 18:22:44 2001 +0100
@@ -97,9 +97,6 @@
 
 (* more about converse rtrancl and trancl, should be merged with main body *)
 
-lemma converse_rtrancl_into_rtrancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R^* \<Longrightarrow> (a,c) \<in> R^*"
-  by (erule rtrancl_induct) (fast intro: rtrancl_into_rtrancl)+
-
 lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
   by (fast intro: trancl_trans)
 




