more notation

[helm.git] / helm / software / matita / library / formal_topology / o-basic_pairs.ma

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 3cd9699acb6cfef6de117427c5fa60d172610c78..e4bf8e5c7f7f4e8a007b2b60c0447650a140f7e4 100644 (file)
--- 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;