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