X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Falgebra%2Fmagmas.ma;h=2366e0fc67a6e0431a38389901bc9e2da23b45bc;hb=3c17c53d6628c1863a33ab071266a0f5614bbce1;hp=caf903ae1c1770c24b903f8cc384e367f8faa887;hpb=f5e6cad85ff6f10b63622a0348ad65492578022e;p=helm.git

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index caf903ae1..2366e0fc6 100644
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -26,7 +26,7 @@ nrecord magma (A: magma_type) : Type[1] ≝
 
 nrecord magma_morphism_type (A,B: magma_type) : Type ≝
  { mmcarr:1> A → B;
-   mmprop: ∀x,y. mmcarr (op ? x y) = op ? (mmcarr x) (mmcarr y)
+   mmprop: ∀x,y. mmcarr (op … x y) = op … (mmcarr x) (mmcarr y)
  }.
 
 nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type ≝
@@ -38,36 +38,36 @@ ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
  λA,B,f,Sa. {y | ∃x. x ∈ Sa ∧ f x = y}.
 
 ndefinition mm_image:
- ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma B.
+ ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma B.
  #A; #B; #Ma; #Mb; #f;
- napply (mk_magma …)
+ napply mk_magma
   [ napply (image … f Ma)
   | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
-    napply (ex_intro …)
+    napply ex_intro
      [ napply (op … x0 y0) 
-     | napply (conj …)
-        [ napply (op_closed …); nassumption
+     | napply conj
+        [ napply op_closed; nassumption
         | nrewrite < Hx1;
           nrewrite < Hy1;
-          napply (mmprop … f …)]##]
+          napply (mmprop … f)]##]
 nqed.
 
 ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
  λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.
  
 ndefinition mm_counter_image:
- ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma A.
+ ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma A.
   #A; #B; #Ma; #Mb; #f;
-  napply (mk_magma …)
+  napply mk_magma
    [ napply (counter_image … f Mb)
    | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
-     napply (ex_intro …)
+     napply ex_intro
       [ napply (op … x0 y0)
-      | napply (conj …)
-         [ napply (op_closed …); nassumption
+      | napply conj
+         [ napply op_closed; nassumption
          | nrewrite < Hx1;
            nrewrite < Hy1;
-           napply (mmprop … f …)]##]
+           napply (mmprop … f)]##]
 nqed.
 
 ndefinition m_intersect: ∀A. magma A → magma A → magma A.
@@ -75,5 +75,5 @@ ndefinition m_intersect: ∀A. magma A → magma A → magma A.
  napply (mk_magma …)
   [ napply (M1 ∩ M2)
   | #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
-    napply (conj …); napply (op_closed …); nassumption ]
+    napply conj; napply op_closed; nassumption ]
 nqed.
\ No newline at end of file