The covering lemma up to a Woodin cardinal

A cardinal kappa is countably closed if mu^omega < kappa whenever mu < kappa. Assume that there is no inner model with a Woodin cardinal and that every set has a sharp. Let K be the core model. Assume that kappa is a countably closed cardinal and that alpha is a successor cardinal of K with kappa < alpha < kappa^+. Then cf( alpha ) = kappa. In particular, K computes successors of countably closed singular cardinals correctly. (The hypothesis of countable closure is not required; see "Weak covering without countable closure", W. J. Mitchell and E. Schimmerling, Math. Res. Lett., Vol. 2, No. 5, Sept. 1995.)