injection sterm

X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_injection.html;h=143c3a293b23537e22d97774ba0c315dfff6df08;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=f6a4b2676256afdf6b403658bfb95ef99f961fd1;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_injection.html b/helm/www/matita/docs/manual/tac_injection.html index f6a4b2676..143c3a293 100644 --- a/helm/www/matita/docs/manual/tac_injection.html +++ b/helm/www/matita/docs/manual/tac_injection.html @@ -1,6 +1,6 @@ -injection sterm

injection sterm
PrevÂ	ChapterÂ 6.Â Tactics	Â Next

injection sterm

injection p

+injection sterm

Matita Home

injection sterm
PrevÂ	ChapterÂ 6.Â Tactics	Â Next

injection sterm

injection p

Pre-conditions:: p must have type K t₁ ... t_n = K t'₁ ... t'_n where both argument lists are empty if K takes no arguments.
Action:: It derives new hypotheses by injectivity of K.
New sequents to prove:: The new sequent to prove is equal to the current sequent