X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcore_notation.moo;h=a2802c3da8eabd6d5bb5176c7323f1e388724c31;hb=da29171d0139bc1be36772084d58b6cbcfdca646;hp=38c1a4efa4c46cd65aa88b0345f905b1ab338b65;hpb=92140306286b05521c7cc49e75c4dae194ccbb52;p=helm.git

diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo
index 38c1a4efa..a2802c3da 100644
--- a/helm/matita/core_notation.moo
+++ b/helm/matita/core_notation.moo
@@ -30,6 +30,30 @@ 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 \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 }.
@@ -54,10 +78,22 @@ notation "a \over b"
   left associative with precedence 55
 for @{ 'divide $a $b }.
 
-notation "- a" 
+notation > "- a" 
   right associative with precedence 60
 for @{ 'uminus $a }.
 
+notation < "- a" 
+  right associative with precedence 75
+for @{ 'uminus $a }.
+
+notation "a !"
+  non associative with precedence 80
+for @{ 'fact $a }.
+
+notation "(a \sup b)"
+  right associative with precedence 65
+for @{ 'exp $a $b}.
+
 notation "\sqrt a" 
   non associative with precedence 60
 for @{ 'sqrt $a }.