changeset 15481 | fc075ae929e4 |
parent 14153 | 76a6ba67bd15 |
child 16417 | 9bc16273c2d4 |
--- a/src/ZF/Epsilon.thy Sun Jan 30 20:48:50 2005 +0100 +++ b/src/ZF/Epsilon.thy Tue Feb 01 18:01:57 2005 +0100 @@ -246,8 +246,7 @@ lemma rank_mono: "a<=b ==> rank(a) le rank(b)" apply (rule subset_imp_le) -apply (subst rank) -apply (subst rank, auto) +apply (auto simp add: rank [of a] rank [of b]) done lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))"