big mess of notation

[helm.git] / helm / software / matita / library / formal_topology / categories.ma

diff --git a/helm/software/matita/library/formal_topology/categories.ma b/helm/software/matita/library/formal_topology/categories.ma
index 30769e5364c27d61d8a0bff9b8a6a6d18d969970..015e245f3f5b142084a4b8a1922e0c07f6b30ade 100644 (file)
--- a/helm/software/matita/library/formal_topology/categories.ma
+++ b/helm/software/matita/library/formal_topology/categories.ma
@@ -511,3 +511,12 @@ definition faithful2 ≝
   λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B).
     ∀o1,o2:A.∀f,g:arrows2 A o1 o2.F⎽⇒ f =_2 F⎽⇒ g → f =_2 g.
     
+
+notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
+notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
+
+notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+
+notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.