X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_generalize.html;h=bcba8c3f9da92f194d2ee60ab034510265bb2733;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=8e03a551f539e9d615ccabd2457396b73f9fb83c;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_generalize.html b/helm/www/matita/docs/manual/tac_generalize.html index 8e03a551f..bcba8c3f9 100644 --- a/helm/www/matita/docs/manual/tac_generalize.html +++ b/helm/www/matita/docs/manual/tac_generalize.html @@ -1,6 +1,6 @@ -generalize <pattern> [as id]
generalize <pattern> [as id]
Prev Chapter 6. Tactics Next

generalize <pattern> [as id]

generalize patt as H

+generalize <pattern> [as id]

generalize <pattern> [as id]
Prev Chapter 6. Tactics Next

generalize <pattern> [as id]

generalize patt as H

Pre-conditions:

All the terms matched by patt must be convertible and close in the context of the current sequent.

Action:

It closes the current sequent by applying a stronger lemma that is proved using the new generated sequent.

New sequents to prove:

It opens a new sequent where the current sequent conclusion