X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fcore_notation.ma;h=54bfd22d512e7917f7102f9c5f7ee165f2695e0c;hb=dbc57c92512c04b3fd88f8289bb8dbe99b2f90e0;hp=4ed9f326c1f239464b335f56964d6027809df4b2;hpb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;p=helm.git diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 4ed9f326c..54bfd22d5 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -111,9 +111,6 @@ for @{ 'congruent $n $m $p }. (* pairs, projections *******************************************************) -notation "hvbox(\langle term 19 a, break term 19 b\rangle)" -with precedence 90 for @{ 'pair $a $b}. - notation "hvbox(x break \times y)" with precedence 70 for @{ 'product $x $y}.