equal
deleted
inserted
replaced
384 by (rewtac Transset_def); |
384 by (rewtac Transset_def); |
385 by (stac Vfrom 1); |
385 by (stac Vfrom 1); |
386 by (Blast_tac 1); |
386 by (Blast_tac 1); |
387 qed "Pow_in_Vfrom"; |
387 qed "Pow_in_Vfrom"; |
388 |
388 |
389 Goal |
389 Goal "[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)"; |
390 "[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)"; |
|
391 (*Blast_tac: PROOF FAILED*) |
390 (*Blast_tac: PROOF FAILED*) |
392 by (fast_tac (claset() addEs [Limit_VfromE] |
391 by (fast_tac (claset() addEs [Limit_VfromE] |
393 addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1); |
392 addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1); |
394 qed "Pow_in_VLimit"; |
393 qed "Pow_in_VLimit"; |
395 |
394 |