X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_letin.html;h=83318bdb5b9421bce11dc1aed226c3e2d801013d;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=97b285b3b423b9319d04448f2c9bb2243665b861;hpb=5b99087bf1b8b8fb1086a72feb6f3fb258a402d8;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_letin.html b/helm/www/matita/docs/manual/tac_letin.html index 97b285b3b..83318bdb5 100644 --- a/helm/www/matita/docs/manual/tac_letin.html +++ b/helm/www/matita/docs/manual/tac_letin.html @@ -1,6 +1,6 @@ -letin id ≝ sterm
letin id ≝ sterm
Prev Chapter 6. Tactics Next

letin id ≝ sterm

letin x ≝ t

+letin id ≝ sterm

letin id ≝ sterm
Prev Chapter 6. Tactics Next

letin id ≝ sterm

letin x ≝ t

Pre-conditions:

None.

Action:

It adds to the context of the current sequent to prove a new definition x ≝ t.

New sequents to prove:

None.

Prev Up Next
left Home normalize <pattern>