X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Fcore_notation.ma;h=12c1a6d7e224ebff92142356b998d81b8e36e8ce;hb=1e15bf5aab8c4d4bdefc1bca9084459a0442a847;hp=098b5d419d4f1620db3ca6e21ff3f96e3a996c80;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git diff --git a/weblib/basics/core_notation.ma b/weblib/basics/core_notation.ma index 098b5d419..12c1a6d7e 100644 --- a/weblib/basics/core_notation.ma +++ b/weblib/basics/core_notation.ma @@ -74,6 +74,8 @@ for @{ 'congruent $n $m $p }. notation "hvbox(\langle term 19 a, break term 19 b\rangle)" with precedence 90 for @{ 'pair $a $b}. +notation "hvbox(〈term 19 a, break term 19 b〉)" +with precedence 90 for @{ 'pair $a $b}. notation "hvbox(x break \times y)" with precedence 70 for @{ 'product $x $y}.