X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_discriminate.html;fp=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_discriminate.html;h=06c9c83333bebcfdd5871ccefb306d4a57d807a5;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=34f6c6aaa5e8aae734c5c575eec1d1088c651fed;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_discriminate.html b/helm/www/matita/docs/manual/tac_discriminate.html index 34f6c6aaa..06c9c8333 100644 --- a/helm/www/matita/docs/manual/tac_discriminate.html +++ b/helm/www/matita/docs/manual/tac_discriminate.html @@ -1,6 +1,6 @@ -discriminate sterm
discriminate sterm
Prev Chapter 6. Tactics Next

discriminate sterm

discriminate p

+discriminate sterm

discriminate sterm
Prev Chapter 6. Tactics Next

discriminate sterm

discriminate p

Pre-conditions:

p must have type K t1 ... tn = K' t'1 ... t'm where K and K' must be different constructors of the same inductive type and each argument list can be empty if its constructor takes no arguments.

Action:

It closes the current sequent by proving the absurdity of p.

New sequents to prove:

None.