X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_reduce.html;h=94120657d1f22619b26db686f27174ef248d3c16;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=309681c9e30bc281e5cd4a7b90e77b902e0ae19d;hpb=5b99087bf1b8b8fb1086a72feb6f3fb258a402d8;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_reduce.html b/helm/www/matita/docs/manual/tac_reduce.html index 309681c9e..94120657d 100644 --- a/helm/www/matita/docs/manual/tac_reduce.html +++ b/helm/www/matita/docs/manual/tac_reduce.html @@ -1,6 +1,6 @@ -reduce <pattern>
reduce <pattern>
Prev Chapter 6. Tactics Next

reduce <pattern>

reduce patt

+reduce <pattern>

reduce <pattern>
Prev Chapter 6. Tactics Next

reduce <pattern>

reduce 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
paramodulation <pattern> Home reflexivity