X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fcategories.ma;h=015e245f3f5b142084a4b8a1922e0c07f6b30ade;hb=c821924472ab07f543c0e4acd0b808715de7a934;hp=30769e5364c27d61d8a0bff9b8a6a6d18d969970;hpb=5fee26d2afb3a67370c92481bfbfdbd9ebed741e;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/categories.ma b/helm/software/matita/library/formal_topology/categories.ma
index 30769e536..015e245f3 100644
--- 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}.