X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-algebra.ma;h=a86d286bc0b034d658e0b34521964795d29d540a;hb=05cfeb82d2624860e66941421a937f308d66cf33;hp=915afc26d5229474d1a92f62bf7d2da959b41d6b;hpb=95ac064b854f31a49f2f8cd3c4b4f4929dc96fc0;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index 915afc26d..a86d286bc 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -324,6 +324,10 @@ coercion ORelation_setoid_of_arrows2_OA.
 
 prefer coercion Type_OF_objs2.
 
+notation > "B ⇒_\o2 C" right associative with precedence 72 for @{'arrows2_OA $B $C}.
+notation "B ⇒\sub (\o 2) C" right associative with precedence 72 for @{'arrows2_OA $B $C}.
+interpretation "'arrows2_OA" 'arrows2_OA A B = (arrows2 OA A B).
+
 (* qui la notazione non va *)
 lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q).
  intros;