X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fnotation%2Fconstructors%2Fdxbind2_3.ma;h=6800d8e5c2f247f9c252e464a7c9fc23a4af1de0;hp=bbded1eabf7e8d6d2242a98e247287f3ed1aa7a6;hb=222044da28742b24584549ba86b1805a87def070;hpb=65008df95049eb835941ffea1aa682c9253c4c2b diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma index bbded1eab..6800d8e5c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma @@ -14,10 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation > "hvbox( T . break ②{ term 46 I } break term 47 T1 )" - non associative with precedence 46 - for @{ 'DxBind2 $T $I $T1 }. - -notation "hvbox( T . break ⓑ { term 46 I } break term 48 T1 )" - non associative with precedence 47 - for @{ 'DxBind2 $T $I $T1 }. +notation "hvbox( L. break ⓑ { term 46 I } break term 49 T1 )" + non associative with precedence 48 + for @{ 'DxBind2 $L $I $T1 }.