some notation for map_arrows2

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
index 6f16b0d3f05f9a0f0812f718e7a3c2066cbb6571..f0e0b712c80caefd132d18b220c6652ed706c975 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -23,10 +23,6 @@ record Obasic_pair: Type2 ≝ {
 interpretation "o-basic pair relation indexed" 'Vdash2 x y c = (Orel c x y).
 interpretation "o-basic pair relation (non applied)" 'Vdash c = (Orel c).
 
-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).
-
 record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝ { 
    Oconcr_rel: (Oconcr BP1) ⇒_\o2 (Oconcr BP2); Oform_rel: (Oform BP1) ⇒_\o2 (Oform BP2);
    Ocommute: ⊩ ∘ Oconcr_rel =_2 Oform_rel ∘ ⊩
@@ -248,4 +244,4 @@ interpretation "Universal pre-image ⊩*" 'rest x = (fun12 ? ? (or_f_star ? ?) (
 
 notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
 notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
-interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 ? ? (or_f_minus ? ?) (Orel x)).
\ No newline at end of file
+interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 ? ? (or_f_minus ? ?) (Orel x)).