]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/hott/notations.ma
update in lib
[helm.git] / matita / matita / lib / hott / notations.ma
index d680e4bd1c0f7d011774f5a7803655220775a106..d2d843cf0ad318d42777e765ba022e369757fa87 100644 (file)
@@ -276,12 +276,6 @@ for @{ 'mem $a $b }.
 notation "hvbox(a break ∉ b)" non associative with precedence 45
 for @{ 'notmem $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)" left associative with precedence 60
 for @{ 'intersects $a $b }. (* \cap *)