X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual-0.5.9%2Ftac_reflexivity.html;fp=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual-0.5.9%2Ftac_reflexivity.html;h=291f0880ad54b5aea48f51e5c6ea9297fd9bb3c3;hb=5b05d943dc8ebfe10e8932795f7f7aa8ef0b4ebc;hp=0000000000000000000000000000000000000000;hpb=7c86bc0cda903d7cac66e2d4cb81bca345b4b5bc;p=helm.git diff --git a/helm/www/matita/docs/manual-0.5.9/tac_reflexivity.html b/helm/www/matita/docs/manual-0.5.9/tac_reflexivity.html new file mode 100644 index 000000000..291f0880a --- /dev/null +++ b/helm/www/matita/docs/manual-0.5.9/tac_reflexivity.html @@ -0,0 +1,6 @@ + +reflexivity
reflexivity
Prev Chapter 7. Tactics Next

reflexivity

reflexivity

+

Synopsis:

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.

+

Prev Up Next
normalize Home replace
\ No newline at end of file