X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcore_notation.moo;h=c528fc111d2041cb83761efa02697a33300b337f;hb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;hp=5b3759cb0eca2c79d2b8117e488fa5989e77f558;hpb=650e3b3c9ff0b9cafb76a0edf8139a53446937ba;p=helm.git

diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo
index 5b3759cb0..c528fc111 100644
--- a/helm/matita/core_notation.moo
+++ b/helm/matita/core_notation.moo
@@ -30,6 +30,22 @@ notation "hvbox(a break \neq b)"
   non associative with precedence 45
 for @{ 'neq $a $b }.
 
+notation "hvbox(a break \nleq b)" 
+  non associative with precedence 45
+for @{ 'nleq $a $b }.
+
+notation "hvbox(a break \ngeq b)" 
+  non associative with precedence 45
+for @{ 'ngeq $a $b }.
+
+notation "hvbox(a break \nless b)" 
+  non associative with precedence 45
+for @{ 'nless $a $b }.
+
+notation "hvbox(a break \ngtr b)" 
+  non associative with precedence 45
+for @{ 'ngtr $a $b }.
+
 notation "hvbox(a break + b)" 
   left associative with precedence 50
 for @{ 'plus $a $b }.
@@ -55,7 +71,7 @@ notation "a \over b"
 for @{ 'divide $a $b }.
 
 notation "- a" 
-  non associative with precedence 60
+  right associative with precedence 60
 for @{ 'uminus $a }.
 
 notation "\sqrt a"