src/HOL/Transitive_Closure.thy
changeset 12566 fe20540bcf93
parent 12428 f3033eed309a
child 12691 d21db58bcdc2
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Dec 20 17:08:55 2001 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Dec 20 18:22:44 2001 +0100
     1.3 @@ -97,9 +97,6 @@
     1.4  
     1.5  (* more about converse rtrancl and trancl, should be merged with main body *)
     1.6  
     1.7 -lemma converse_rtrancl_into_rtrancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R^* \<Longrightarrow> (a,c) \<in> R^*"
     1.8 -  by (erule rtrancl_induct) (fast intro: rtrancl_into_rtrancl)+
     1.9 -
    1.10  lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
    1.11    by (fast intro: trancl_trans)
    1.12