I'd like to check with my colleagues whether I have correctly understood "embedded resolution of singularities".

Let $X$ be a nonsingular projective variety over $\mathbf C$ and let $D$ be a "nice" divisor on $X$, say $D$ has strictly normal crossings. (Maybe we could just take $D$ to be a closed subscheme?)

Then, has the following statement been proven? And what is a "good" reference?

There exists a projective birational surjective morphism $\psi:Y\to X$ with $Y$ a nonsingular projective variety over $\mathbf C$ and the inverse image of $D$ in $Y$ a nonsingular projective variety over $\mathbf C$ of codimension one in $Y$?

I'm worried about whether I have correctly understood this statement, or maybe one needs some "normality" conditions on $D$ to assure this "embedded" resolution of singularities.

Also, how does one obtain this embedded resolution of singularities? Can we write down a terminating process which ends with an embedded resolution of singularities?

I have a hard time "believing" the above statement, but I don't know why. If anybody can explain to me that this is not so surprising as a result I would be very thankful.

strict transformof $D$ to be smooth; in general the inverse image of $D$ (i.e. the total transform) will be a normal crossing divisor. See en.wikipedia.org/wiki/Resolution_of_singularities, in particular the section Definitions and the bibliography. Also look at this nice expository paper by Hauser ams.org/journals/bull/2003-40-03/S0273-0979-03-00982-0 – Francesco Polizzi Feb 1 '13 at 15:49