src/HOL/Transitive_Closure.thy
changeset 14398 c5c47703f763
parent 14361 ad2f5da643b4
child 14404 4952c5a92e04
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Feb 19 10:41:32 2004 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Feb 19 15:57:34 2004 +0100
     1.3 @@ -129,7 +129,7 @@
     1.4  
     1.5  lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*"
     1.6    apply (drule rtrancl_mono)
     1.7 -  apply (drule rtrancl_mono, simp, blast)
     1.8 +  apply (drule rtrancl_mono, simp)
     1.9    done
    1.10  
    1.11  lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*"