Matita Home
whd <pattern>
Prev
Chapter 6. Tactics
Next
whd <pattern>
whd patt
Pre-conditions:
None.
Action:
It replaces all the terms matched by
patt
with their βδιζ-weak-head normal form.
New sequents to prove:
None.
Matita Home