X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_left.html;h=623ced5f250ac9d7bc6a61c726b3b92e8ab3afd2;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=65298b52f54c7b5b2417ea35358371bd66fd2e28;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_left.html b/helm/www/matita/docs/manual/tac_left.html index 65298b52f..623ced5f2 100644 --- a/helm/www/matita/docs/manual/tac_left.html +++ b/helm/www/matita/docs/manual/tac_left.html @@ -1,6 +1,6 @@ -left
left
Prev Chapter 6. Tactics Next

left

left

+left

left
Prev Chapter 6. Tactics Next

left

left

Pre-conditions:

The conclusion of the current sequent must be an inductive type or the application of an inductive type with at least one constructor.

Action:

Equivalent to constructor 1.

New sequents to prove:

It opens a new sequent for each premise of the first