equal
deleted
inserted
replaced
145 apply (erule Ord_succ) |
145 apply (erule Ord_succ) |
146 done |
146 done |
147 |
147 |
148 lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))" |
148 lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))" |
149 apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst]) |
149 apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst]) |
150 apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst]) |
150 apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst]) |
151 apply (subst rank_succ) |
151 apply (subst rank_succ) |
152 apply (rule Ord_rank [THEN Vfrom_succ_lemma]) |
152 apply (rule Ord_rank [THEN Vfrom_succ_lemma]) |
153 done |
153 done |
154 |
154 |
155 (*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces |
155 (*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces |