X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_tactics.ma;h=882bdcbeb1e89856ea2954c81875382ef463a2de;hb=0f13d14b63b012e0ea8ce0d0e71bf808fdd444eb;hp=cf1bbe14abd2474460d50a06ae368ab82b02e23e;hpb=6901cc3ca6c2ceb1250fbfce10e632a9af1e9603;p=helm.git diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma index cf1bbe14a..882bdcbeb 100644 --- a/helm/software/matita/tests/ng_tactics.ma +++ b/helm/software/matita/tests/ng_tactics.ma @@ -31,7 +31,7 @@ nwhd in H: (?%? (?%?)); nchange in match (S ?) in H:(??%?) ⊢ (??%%) with (pred (S ?)); ngeneralize in match H; napply (? H); -nelim m in ⊢ (???(?%?) → %); (*SBAGLIA UNIFICATORE*) +nelim m in ⊢ (???(?%?) → %); nnormalize; ##[ ncases x in H ⊢ (? → % → ?); ##|