equal
deleted
inserted
replaced
389 by (Blast_tac 1); |
389 by (Blast_tac 1); |
390 qed "Pow_in_Vfrom"; |
390 qed "Pow_in_Vfrom"; |
391 |
391 |
392 goal Univ.thy |
392 goal Univ.thy |
393 "!!a. [| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)"; |
393 "!!a. [| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)"; |
394 by (blast_tac (claset() addEs [Limit_VfromE] |
394 (*Blast_tac: PROOF FAILED*) |
|
395 by (fast_tac (claset() addEs [Limit_VfromE] |
395 addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1); |
396 addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1); |
396 qed "Pow_in_VLimit"; |
397 qed "Pow_in_VLimit"; |
397 |
398 |
398 |
399 |
399 (*** The set Vset(i) ***) |
400 (*** The set Vset(i) ***) |