X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fo-algebra.ma;h=fb508aa92b23c61b90dc280ab72297416ca177d9;hb=a823c605d3a541c8d7df2bcc3c21bf459c9d25c4;hp=67ff5140e1f12fddc135b00a193b5a817913086c;hpb=5fee26d2afb3a67370c92481bfbfdbd9ebed741e;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/o-algebra.ma b/helm/software/matita/library/formal_topology/o-algebra.ma
index 67ff5140e..fb508aa92 100644
--- a/helm/software/matita/library/formal_topology/o-algebra.ma
+++ b/helm/software/matita/library/formal_topology/o-algebra.ma
@@ -241,21 +241,12 @@ intros; apply (or_f ?? c);
 qed.
 coercion arrows1_of_ORelation_setoid.
 
-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}.
-
 interpretation "o-relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (or_f_minus_star ? ?) r).
 interpretation "o-relation f⎻" 'OR_f_minus r = (fun12 ?? (or_f_minus ? ?) r).
 interpretation "o-relation f*" 'OR_f_star r = (fun12 ?? (or_f_star ? ?) r).
 
 definition or_prop1 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q.
-   (F p ≤ q) = (p ≤ F* q).
+   (F p ≤ q) =_1 (p ≤ F* q).
 intros; apply (or_prop1_ ?? F p q);
 qed.