From 6d46de64db7b1fee5ab0784fd5b710dbe6d3a9e5 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Thu, 15 Mar 2012 10:33:00 +0000 Subject: [PATCH] Manual commit (basics/core_notation.ma) --- weblib/basics/core_notation.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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}. -- 2.39.2