X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_inversion.html;h=ab2e5c36c61b45106799aca7581625d2e7c2a3ed;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=ea424be3efd9df04fa0f2ede14b69054a1d397c4;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_inversion.html b/helm/www/matita/docs/manual/tac_inversion.html index ea424be3e..ab2e5c36c 100644 --- a/helm/www/matita/docs/manual/tac_inversion.html +++ b/helm/www/matita/docs/manual/tac_inversion.html @@ -1,6 +1,6 @@ -inversion sterm
inversion sterm
Prev Chapter 6. Tactics Next

inversion sterm

inversion t

+inversion sterm

inversion sterm
Prev Chapter 6. Tactics Next

inversion sterm

inversion t

Pre-conditions:

The type of the term t must be an inductive type or the application of an inductive type.

Action:

It proceeds by cases on t paying attention to the constraints imposed by the actual "right arguments"