\ldots used here and there. Cool!

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 842cfceb93c0aa82f50878294937479361911714..caf903ae1c1770c24b903f8cc384e367f8faa887 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -40,16 +40,16 @@ ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
 ndefinition mm_image:
  ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma B.
  #A; #B; #Ma; #Mb; #f;
- napply (mk_magma ???)
-  [ napply (image ?? f Ma)
+ napply (mk_magma …)
+  [ napply (image … f Ma)
   | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
-    napply (ex_intro ????)
-     [ napply (op ? x0 y0) 
-     | napply (conj ????)
-        [ napply (op_closed ??????); nassumption
+    napply (ex_intro …)
+     [ napply (op … x0 y0) 
+     | 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 ≝
@@ -58,22 +58,22 @@ ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
 ndefinition mm_counter_image:
  ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma A.
   #A; #B; #Ma; #Mb; #f;
-  napply (mk_magma ???)
-   [ napply (counter_image ?? f Mb)
+  napply (mk_magma …)
+   [ napply (counter_image … f Mb)
    | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
-     napply (ex_intro ????)
-      [ napply (op ? x0 y0)
-      | napply (conj ????)
-         [ napply (op_closed ??????); nassumption
+     napply (ex_intro …)
+      [ napply (op … x0 y0)
+      | 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.
  #A; #M1; #M2;
- napply (mk_magma ???)
+ 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

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index ed2973d87af9170b0a910a747f42f64f343e8ce6..9d31b09439dc29f0b12eb9550140f9918f41ac3a 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -37,14 +37,14 @@ nrecord function_space (A,B: setoid): Type ≝
  }.
 
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
-(*
+
 ndefinition function_space_setoid: setoid → setoid → setoid.
  #A; #B; napply (mk_setoid ?????);
 ##[ napply (function_space A B);
 ##| #f; #f1; napply (∀a:A. proofs (eq ? (f a) (f1 a)));
 ##| nwhd; #x; #a;
     napply (f_ok ? ? x ? ? ?); (* QUI!! *)
-    unfold carr; unfold proofs; simplify;
+(*    unfold carr; unfold proofs; simplify;
     apply (refl A)
   | simplify;
     intros;

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 07c7884ce7fc35cd153630ad059c181d3cee789d..3f5a4feeeceb634c199b7b7c8727c3289f729025 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -32,7 +32,7 @@ nqed.
 
 ntheorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
  #A; #S1; #S2; #S3; #H12; #H23; #x; #H;
- napply (H23 ??); napply (H12 ??); nassumption;
+ napply (H23 …); napply (H12 …); nassumption;
 nqed.
 
 ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.