X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_normalize.html;h=4d1364cefeaede86f0eb227f17213dfcbcfa21c6;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=f4a60120bc75f8c901a4099d834c7565f8a712e2;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_normalize.html b/helm/www/matita/docs/manual/tac_normalize.html index f4a60120b..4d1364cef 100644 --- a/helm/www/matita/docs/manual/tac_normalize.html +++ b/helm/www/matita/docs/manual/tac_normalize.html @@ -1,6 +1,6 @@ -normalize <pattern>
normalize <pattern>
Prev Chapter 6. Tactics Next

normalize <pattern>

normalize patt

+normalize <pattern>

normalize <pattern>
Prev Chapter 6. Tactics Next

normalize <pattern>

normalize patt

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 id ≝ sterm Home paramodulation <pattern>