X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fnotation%2Frelations%2Frdropstar_3.ma;h=85ce21e3de4c66d6faca1f6fda0f2f49dba7e31e;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=14803b14f59b5de713adb22b7ddf7bd82248b0d7;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_3.ma index 14803b14f..85ce21e3d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⇩ * [ term 46 e ] break term 46 L1 ≡ break term 46 L2 )" +notation "hvbox( ⬇ * [ term 46 e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDropStar $e $L1 $L2 }.