X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_whd.html;h=25190ce3e871694e272eabc868090927b5d6b783;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=636ff383a62b329ffc89347a0b30c637f0c65c6d;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_whd.html b/helm/www/matita/docs/manual/tac_whd.html index 636ff383a..25190ce3e 100644 --- a/helm/www/matita/docs/manual/tac_whd.html +++ b/helm/www/matita/docs/manual/tac_whd.html @@ -1,6 +1,6 @@ -whd <pattern>
whd <pattern>
Prev Chapter 6. Tactics Next

whd <pattern>

whd patt

+whd <pattern>

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.

Prev Up Next
unfold [sterm] <pattern> Home Chapter 7. Tacticals