X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_unfold.html;h=0f23f268e232a52367f7caa4ef3cc97edd758645;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=120ce67d38bbc7f0d096f6385c27be4290fe4c73;hpb=5b99087bf1b8b8fb1086a72feb6f3fb258a402d8;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_unfold.html b/helm/www/matita/docs/manual/tac_unfold.html index 120ce67d3..0f23f268e 100644 --- a/helm/www/matita/docs/manual/tac_unfold.html +++ b/helm/www/matita/docs/manual/tac_unfold.html @@ -1,6 +1,6 @@ -unfold [sterm] <pattern>
unfold [sterm] <pattern>
Prev Chapter 6. Tactics Next

unfold [sterm] <pattern>

unfold t patt

+unfold [sterm] <pattern>

unfold [sterm] <pattern>
Prev Chapter 6. Tactics Next

unfold [sterm] <pattern>

unfold t patt

Pre-conditions:

None.

Action:

It finds all the occurrences of t (possibly applied to arguments) in the subterms matched by patt. Then it δ-expands each occurrence,