- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / contribs / dama / dama_didactic / reals.ma

diff --git a/matita/matita/contribs/dama/dama_didactic/reals.ma b/matita/matita/contribs/dama/dama_didactic/reals.ma
index 4dffb53fb45000d9ea2bc76524486d5b36e5d90d..1474d4b7d01deb80989b7b0f151f278b47531397 100644 (file)
--- a/matita/matita/contribs/dama/dama_didactic/reals.ma
+++ b/matita/matita/contribs/dama/dama_didactic/reals.ma
@@ -32,7 +32,7 @@ interpretation "real plus" 'plus x y = (Rplus x y).
 interpretation "real opp" 'uminus x = (Ropp x). 
 
 notation "hvbox(a break · b)"
-  right associative with precedence 55
+  right associative with precedence 60
 for @{ 'mult $a $b }.
 
 interpretation "real mult" 'mult x y = (Rmult x y).