normalize
Prev Chapter 7. Tactics Next

normalize

normalize patt

Synopsis:

normalize pattern

Pre-conditions:

None.

Action:

It replaces all the terms matched by patt with their βδιζ-normal form.

New sequents to prove:

None.

Prev Up Next
letin Home reflexivity