]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
nasty change in the lexer/parser:
[helm.git] / helm / software / matita / contribs / formal_topology / overlap / r-o-basic_pairs.ma
index a50ed8cc26a5d505876a9c48ca7ebf76f1417145..310ef55ebf53f23dbd552cda169685204ec5b17b 100644 (file)
@@ -94,7 +94,7 @@ lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
 qed.
 
 notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
-interpretation "map arrows 2" 'map_arrows F x = (fun12 _ _ (map_arrows2 _ _ F _ _) x).
+interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
 
 definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
 intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);