X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fo-basic_pairs.ma;h=e4bf8e5c7f7f4e8a007b2b60c0447650a140f7e4;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=3cd9699acb6cfef6de117427c5fa60d172610c78;hpb=1ed4fe0f28d3b0b915387330cd722bfb80fb1063;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/o-basic_pairs.ma b/helm/software/matita/library/formal_topology/o-basic_pairs.ma
index 3cd9699ac..e4bf8e5c7 100644
--- a/helm/software/matita/library/formal_topology/o-basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/o-basic_pairs.ma
@@ -179,6 +179,10 @@ definition Orelation_pair_setoid_of_arrows2_OBP:
   ∀P,Q.arrows2 OBP P Q → Orelation_pair_setoid P Q ≝ λP,Q,c.c.
 coercion Orelation_pair_setoid_of_arrows2_OBP.
 
+notation > "B ⇒_\obp2 C" right associative with precedence 72 for @{'arrows2_OBP $B $C}.
+notation "B ⇒\sub (\obp 2) C" right associative with precedence 72 for @{'arrows2_OBP $B $C}.
+interpretation "'arrows2_OBP" 'arrows2_OBP A B = (arrows2 OBP A B).
+
 (*
 definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
  intros; constructor 1;