more work, but russell too slow

[helm.git] / helm / software / matita / contribs / dama / dama / cprop_connectives.ma

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index aabf6e79e08906331e8883e659a79f6c5ac19f6c..a0a701694ccc9ba1c7bac93758cfb3b0527ef261 100644 (file)
--- 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 ≝