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