X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcore_notation.moo;h=c30e5142c08d6380890a4d6b6e7b955636238542;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=9af57e4fe90b25c71a152c6b0db611a060d98a35;hpb=373b88228a8f9a6b4b4dcf781bc166865f89f43d;p=helm.git

diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo
index 9af57e4fe..c30e5142c 100644
--- a/helm/matita/core_notation.moo
+++ b/helm/matita/core_notation.moo
@@ -46,6 +46,14 @@ notation "hvbox(a break \ngtr b)"
   non associative with precedence 45
 for @{ 'ngtr $a $b }.
 
+notation "hvbox(a break \divides b)"
+  non associative with precedence 45
+for @{ 'divides $a $b }.
+
+notation "hvbox(a break \ndivides b)"
+  non associative with precedence 45
+for @{ 'ndivides $a $b }.
+
 notation "hvbox(a break + b)" 
   left associative with precedence 50
 for @{ 'plus $a $b }.
@@ -58,9 +66,9 @@ notation "hvbox(a break * b)"
   left associative with precedence 55
 for @{ 'times $a $b }.
 
-notation "hvbox(a break / b)" 
+notation "hvbox(a break \mod b)" 
   left associative with precedence 55
-for @{ 'divide $a $b }.
+for @{ 'module $a $b }.
 
 notation "\frac a b" 
   non associative with precedence 90
@@ -70,12 +78,20 @@ notation "a \over b"
   left associative with precedence 55
 for @{ 'divide $a $b }.
 
-notation "- a" 
+notation "hvbox(a break / b)" 
+  left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation > "- a" 
   right associative with precedence 60
 for @{ 'uminus $a }.
 
+notation < "- a" 
+  right associative with precedence 75
+for @{ 'uminus $a }.
+
 notation "a !"
-  left associative with precedence 65
+  non associative with precedence 80
 for @{ 'fact $a }.
 
 notation "(a \sup b)"