equal
deleted
inserted
replaced
68 apply (rule_tac a=x in eps_induct) |
68 apply (rule_tac a=x in eps_induct) |
69 apply (subst Vfrom) |
69 apply (subst Vfrom) |
70 apply (subst Vfrom) |
70 apply (subst Vfrom) |
71 apply (rule subset_refl [THEN Un_mono]) |
71 apply (rule subset_refl [THEN Un_mono]) |
72 apply (rule UN_least) |
72 apply (rule UN_least) |
73 txt{*expand rank(x1) = (\<Union>y\<in>x1. succ(rank(y))) in assumptions*} |
73 txt{*expand @{text "rank(x1) = (\<Union>y\<in>x1. succ(rank(y)))"} in assumptions*} |
74 apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E]) |
74 apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E]) |
75 apply (rule subset_trans) |
75 apply (rule subset_trans) |
76 apply (erule_tac [2] UN_upper) |
76 apply (erule_tac [2] UN_upper) |
77 apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono]) |
77 apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono]) |
78 apply (erule ltI [THEN le_imp_subset]) |
78 apply (erule ltI [THEN le_imp_subset]) |