From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Thu, 15 Mar 2012 10:33:00 +0000 (+0000)
Subject: Manual commit (basics/core_notation.ma)
X-Git-Tag: make_still_working~1853
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=6d46de64db7b1fee5ab0784fd5b710dbe6d3a9e5

Manual commit (basics/core_notation.ma)
---

diff --git a/weblib/basics/core_notation.ma b/weblib/basics/core_notation.ma
index 12c1a6d7e..bc4cc21c9 100644
--- a/weblib/basics/core_notation.ma
+++ b/weblib/basics/core_notation.ma
@@ -74,7 +74,7 @@ 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〉)"
+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
@@ -286,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}.