]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/formal_topology/r-o-basic_pairs.ma
- labelled sequential reduction started ...
[helm.git] / matita / matita / lib / formal_topology / r-o-basic_pairs.ma
index 76d077cfa03cc8e2b7d5cd1fe564c5a5d5f7b0ec..0218ed8359bdf7d1cbdd5bf3b31acc3fe2303149 100644 (file)
@@ -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].