whd pattern [nodelta]

None.

It replaces all the terms matched by patt with their βδιζ-weak-head normal form. If nodelta is specified, δ-expansions are not performed.

None.