X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_reflexivity.html;fp=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_reflexivity.html;h=bbd9e3e32df223fa1b367235e7d16d73e1d311e3;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=1afd09b380eb08db2592a5319dc7f916080fdca2;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_reflexivity.html b/helm/www/matita/docs/manual/tac_reflexivity.html index 1afd09b38..bbd9e3e32 100644 --- a/helm/www/matita/docs/manual/tac_reflexivity.html +++ b/helm/www/matita/docs/manual/tac_reflexivity.html @@ -1,6 +1,6 @@ -reflexivity
reflexivity
Prev Chapter 6. Tactics Next

reflexivity

reflexivity

+reflexivity

reflexivity
Prev Chapter 6. Tactics Next

reflexivity

reflexivity

Pre-conditions:

The conclusion of the current sequent must be t=t for some term t

Action:

It closes the current sequent by reflexivity of equality.

New sequents to prove:

None.