whd patt
whd pattern
None.
It replaces all the terms matched by patt with their βδιζ-weak-head normal form.
Matita HomeMatita Home