X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fcprop_connectives.ma;h=a0a701694ccc9ba1c7bac93758cfb3b0527ef261;hb=25aa80d913c903fcc270d05464cf3084b12d52a8;hp=aabf6e79e08906331e8883e659a79f6c5ac19f6c;hpb=ada8695ba51b2ecbd4a955f990e8d06f038aac6b;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index aabf6e79e..a0a701694 100644
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -54,7 +54,8 @@ interpretation "pair pi2" 'pi2a x = (second _ _ x).
 interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
 interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
 
-notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
+with precedence 90 for @{ 'pair $a $b}.
 interpretation "pair" 'pair a b = (pair _ _ a b).
 
 inductive exT (A:Type) (P:A→CProp) : CProp ≝