X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_split.html;h=00ffcd154ff1f262bda9691e57568a5d57bd1273;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=52872dc7ed4944e676aca64cf84f63cabd7a03bf;hpb=5b99087bf1b8b8fb1086a72feb6f3fb258a402d8;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_split.html b/helm/www/matita/docs/manual/tac_split.html index 52872dc7e..00ffcd154 100644 --- a/helm/www/matita/docs/manual/tac_split.html +++ b/helm/www/matita/docs/manual/tac_split.html @@ -1,6 +1,6 @@ -split
split
Prev Chapter 6. Tactics Next

split

split

+split

split
Prev Chapter 6. Tactics Next

split

split

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