X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_exact.html;fp=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_exact.html;h=37a49619dcb4023637c444647874a711e3e2f665;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=b7e7d7e8cd2601b8d19ba6b820c998524b8f8254;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_exact.html b/helm/www/matita/docs/manual/tac_exact.html index b7e7d7e8c..37a49619d 100644 --- a/helm/www/matita/docs/manual/tac_exact.html +++ b/helm/www/matita/docs/manual/tac_exact.html @@ -1,6 +1,6 @@ -exact sterm
exact sterm
Prev Chapter 6. Tactics Next

exact sterm

exact p

+exact sterm

exact sterm
Prev Chapter 6. Tactics Next

exact sterm

exact p

Pre-conditions:

The type of p must be convertible with the conclusion of the current sequent.

Action:

It closes the current sequent using p.

New sequents to prove:

None.

Prev Up Next
elimType sterm [using sterm] [<intros_spec>] Home exists