X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_intro.html;h=f99fdb346c5b21822948935ceaac6af7098f4058;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=6361dd0793739a874639dea1d643ba78a41ba746;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_intro.html b/helm/www/matita/docs/manual/tac_intro.html index 6361dd079..f99fdb346 100644 --- a/helm/www/matita/docs/manual/tac_intro.html +++ b/helm/www/matita/docs/manual/tac_intro.html @@ -1,6 +1,6 @@ -intro [id]
intro [id]
Prev Chapter 6. Tactics Next

intro [id]

intro H

+intro [id]

intro [id]
Prev Chapter 6. Tactics Next

intro [id]

intro H

Pre-conditions:

The conclusion of the sequent to prove must be an implication or a universal quantification.

Action:

It applies the right introduction rule for implication, closing the current sequent.

New sequents to prove:

It opens a new sequent to prove adding to the hypothesis