X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fr-o-basic_pairs.ma;h=0218ed8359bdf7d1cbdd5bf3b31acc3fe2303149;hb=2b51cf74b9a5f37d0f91780ceae4b8f4d0ee38a1;hp=76d077cfa03cc8e2b7d5cd1fe564c5a5d5f7b0ec;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git diff --git a/matita/matita/lib/formal_topology/r-o-basic_pairs.ma b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma index 76d077cfa..0218ed835 100644 --- a/matita/matita/lib/formal_topology/r-o-basic_pairs.ma +++ b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma @@ -93,7 +93,7 @@ lemma curry: ∀A,B,C.(A × B ⇒_1 C) → A → (B ⇒_1 C). | intros; apply (#‡e); ] qed. -notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}. +notation < "F x" left associative with precedence 65 for @{'map_arrows $F $x}. interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x). definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp[1].