X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcore_notation.moo;h=b201a0555125bb15c2fa634433e74a64bfa3fe44;hb=f2d9db85559c7a8db11aae1153495fae4a258d54;hp=ed0c7007beb4e5384bf19097347e689bef0e4c17;hpb=fa3ef782b1336310a78868e7dfc900fa988ee2ab;p=helm.git

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index ed0c7007b..b201a0555 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -94,6 +94,10 @@ notation "hvbox(a break * b)"
   left associative with precedence 55
 for @{ 'times $a $b }.
 
+notation "hvbox(a break \middot b)" 
+  left associative with precedence 55
+  for @{ 'middot $a $b }.
+
 notation "hvbox(a break \mod b)" 
   left associative with precedence 55
 for @{ 'module $a $b }.
@@ -117,10 +121,6 @@ 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 }.
@@ -136,3 +136,52 @@ for @{ 'and $a $b }.
 notation "hvbox(\lnot a)" 
   non associative with precedence 40
 for @{ 'not $a }.
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" non associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" non associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45 
+  for @{ 'napart $a $b}.
+        
+notation "hvbox(a break # b)" non associative with precedence 45 
+  for @{ 'apart $a $b}.
+    
+notation "hvbox(a break \circ b)" 
+  left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}.
+notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }.
+notation < "s \sup (-1) x" with precedence 60 for @{ 'invert_appl $s $x}. 
+
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)