X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fhtml%2Ftac_cut.html;fp=matita%2Fmatita%2Fhelp%2FC%2Fhtml%2Ftac_cut.html;h=7484b50aecf722359914f0097915af4aa6c95e01;hb=9d5a0d55e331b348d44b6d50d3d67e62b60a0e18;hp=0000000000000000000000000000000000000000;hpb=7b6ca76a0ed511b288b654729c9758277dbcd352;p=helm.git diff --git a/matita/matita/help/C/html/tac_cut.html b/matita/matita/help/C/html/tac_cut.html new file mode 100644 index 000000000..7484b50ae --- /dev/null +++ b/matita/matita/help/C/html/tac_cut.html @@ -0,0 +1,8 @@ + +cut
cut
Prev Chapter 7. Tactics Next

cut

cut P

+

Synopsis:

cut sterm

Pre-conditions:

P must be a type.

Action:

It closes the current sequent.

New sequents to prove:

It opens two new sequents. The first one has conclusion + P → G where G is the + old conclusion. + The second sequent has conclusion P and + hypotheses the hypotheses of the current sequent to prove.

+

Prev Up Next
change Home destruct
\ No newline at end of file