X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fnotation%2Frelations%2Fblack_rightarrow_4.ma;h=f27fa0bad0a29d40d4a3a66f9e27263cb60d5f59;hb=2bc0ba993e26ab77a792b38ba39da7a3dd03ad43;hp=8622760f3315822075397736bc46f4118988cc4e;hpb=873fb39bdd21aa14877bf5d50db26e3a050c6d43;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma index 8622760f3..f27fa0bad 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( t1 ➡ 'd' 'f' [ break term 46 p, break term 46 q ] break term 46 t2 )" +notation "hvbox( t1 ➡'d''f'[ break term 46 p, break term 46 q ] break term 46 t2 )" non associative with precedence 45 for @{ 'BlackRightArrow $t1 $p $q $t2 }.