X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;h=3512ad6fe0b59697b526384ad8a7d09aaf559522;hb=325bc2fb36e8f8db99a152037d71332c9ac7eff9;hp=a425dfcc357783ee52a23f8215be3d91265d29b5;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/matita/library/demo/power_derivative.ma b/matita/matita/library/demo/power_derivative.ma index a425dfcc3..3512ad6fe 100644 --- a/matita/matita/library/demo/power_derivative.ma +++ b/matita/matita/library/demo/power_derivative.ma @@ -213,11 +213,11 @@ interpretation "Rderivative" 'derivative f = (derivative f). * Any file that includes this one can not use 'x' as an identifier *) notation "hvbox('X' \sup n)" - non associative with precedence 60 + non associative with precedence 65 for @{ 'monomio $n }. notation "hvbox('X')" - non associative with precedence 60 + non associative with precedence 65 for @{ 'monomio 1 }. interpretation "Rmonomio" 'monomio n = (monomio n).