X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids.ma;h=376edc0ceb8fdfdbda4399c046a49bb50ff57eb5;hb=90ff94e74ceed0954b8599bff55d5c84f15c1b9f;hp=e593ea7d52be439e22b776a8c5d81aa334547f3f;hpb=e8fbe5898b3214a5b0c4d48e8c9d1ee55f3415cc;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index e593ea7d5..376edc0ce 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -28,6 +28,9 @@ unification hint 0 ≔ R : setoid;
 (* ---------------------------------------- *) ⊢ 
    setoid ≡ force1 ? MR lock.
 
+notation < "[\setoid\ensp\of term 19 x]" non associative with precedence 90 for @{'mk_setoid $x}.
+interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
+
 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
 
 notation > "hvbox(a break =_0 b)" non associative with precedence 45
@@ -80,7 +83,7 @@ nlemma unary_morph_eq: ∀A,B.∀f,g:A ⇒_0 B. (∀x. f x = g x) → f = g.
 nlemma mk_binary_morphism:
  ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
   A ⇒_0 (unary_morph_setoid B C).
- #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
+ #A; #B; #C; #f; #H; @; ##[ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
  /2/.
 nqed.
 
@@ -96,10 +99,10 @@ ndefinition comp_unary_morphisms:
 nqed.
 
 unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
-   R ≟ mk_unary_morphism ?? (composition … f g)
+   R ≟ mk_unary_morphism ?? (composition ??? f g)
         (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun1 ?? R ≡ (composition … f g).
+                              fun1 ?? R ≡ (composition ??? f g).
 
 ndefinition comp_binary_morphisms: 
   ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).