- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / library / didactic / exercises / natural_deduction_theories.ma

diff --git a/matita/matita/library/didactic/exercises/natural_deduction_theories.ma b/matita/matita/library/didactic/exercises/natural_deduction_theories.ma
index 9768e26e2997da01f7c6b1da99a4cdff2ae1c174..7d5d893785850068212c66d7fab7aa5fe0c1b621 100644 (file)
--- a/matita/matita/library/didactic/exercises/natural_deduction_theories.ma
+++ b/matita/matita/library/didactic/exercises/natural_deduction_theories.ma
@@ -197,8 +197,8 @@ interpretation "=" 'my_eq x y = (eq x y).
 interpretation "S" 'my_S x = (S x).
 interpretation "O" 'my_O = O.
 
-notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}.
-notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}.
+notation "x + y" non associative with precedence 55 for @{'my_plus $x $y}.
+notation "x * y" non associative with precedence 60 for @{'my_mult $x $y}.
 notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}.
 notation > "'S' x" non associative with precedence 40 for @{'my_S $x}.
 notation < "'S'  x" non associative with precedence 40 for @{'my_S $x}.