X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_cut.html;h=dd9550209dffd905e99a2171ace59eacb7373824;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=fa956c4418b7e87e50bc6b40c46e59517918725c;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_cut.html b/helm/www/matita/docs/manual/tac_cut.html index fa956c441..dd9550209 100644 --- a/helm/www/matita/docs/manual/tac_cut.html +++ b/helm/www/matita/docs/manual/tac_cut.html @@ -1,6 +1,6 @@ -cut sterm [as id]
cut sterm [as id]
Prev Chapter 6. Tactics Next

cut sterm [as id]

cut P as H

+cut sterm [as id]

cut sterm [as id]
Prev Chapter 6. Tactics Next

cut sterm [as id]

cut P as H

Pre-conditions:

P must have type Prop.

Action:

It closes the current sequent.

New sequents to prove:

It opens two new sequents. The first one has an extra hypothesis H:P. If H is omitted, the name of the hypothesis is automatically generated.