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

transitivity

transitivity t

+

Synopsis:

transitivity sterm

Pre-conditions:

The conclusion of the current proof must be an equality.

Action:

It closes the current sequent by transitivity of the equality.

New sequents to prove:

It opens two new sequents l=t and + t=r where l and r are the left and right hand side of the equality in the conclusion of +the current sequent to prove.

+

Prev Up Next
symmetry Home unfold
\ No newline at end of file