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

lapply

+ lapply t +

+

Synopsis:

+ lapply + sterm +

Pre-conditions:

None.

Action:

+ It generalizes the conclusion of the current goal + adding as a premise the type of t, + closing the current goal. +

New sequents to prove:

+ The new sequent has conclusion T → G where + T is the type of t + and G the old conclusion. +

+

Prev Up Next
inversion Home letin
\ No newline at end of file