X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Fcore_notation.ma;h=bc4cc21c925400a8ae63640ec1d40d039ae37c9a;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=098b5d419d4f1620db3ca6e21ff3f96e3a996c80;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/basics/core_notation.ma b/weblib/basics/core_notation.ma
index 098b5d419..bc4cc21c9 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}.
@@ -284,4 +286,4 @@ notation > "⊩ " with precedence 60 for @{'Vdash ?}.
 notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
 
 notation < "maction (mstyle color #ff0000 (­…­)) (t)" 
-non associative with precedence 90 for @{'hide $t}.
\ No newline at end of file
+non associative with precedence 90 for @{'hide $t}.