From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jul 2009 12:18:26 +0000 (+0000)
Subject: More \ldots.
X-Git-Tag: make_still_working~3591
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=70893c71a58e7788b9ec2256dd96f3d75818b61a;p=helm.git

More \ldots.
---

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index caf903ae1..74663f45a 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,7 +38,7 @@ 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 (image … f Ma)
@@ -56,7 +56,7 @@ 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 (counter_image … f Mb)
diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index 9d31b0943..40982a660 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -18,13 +18,13 @@ include "properties/relations.ma".
 nrecord setoid : Type[1] ≝
  { carr:> Type;
    eq: carr → carr → CProp;
-   refl: reflexive ? eq;
-   sym: symmetric ? eq;
-   trans: transitive ? eq
+   refl: reflexive … eq;
+   sym: symmetric … eq;
+   trans: transitive … eq
  }.
 
 ndefinition proofs: CProp → setoid.
-#P; napply (mk_setoid ?????);
+#P; napply (mk_setoid …);
 ##[ napply P;
 ##| #x; #y; napply True;
 ##|##*: nwhd; nrepeat (#_); napply I;
@@ -33,17 +33,17 @@ nqed.
 
 nrecord function_space (A,B: setoid): Type ≝
  { f:1> A → B;
-   f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
+   f_ok: ∀a,a':A. proofs (eq … a a') → proofs (eq … (f a) (f a'))
  }.
 
 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 ?????);
+ #A; #B; napply (mk_setoid …);
 ##[ napply (function_space A B);
-##| #f; #f1; napply (∀a:A. proofs (eq ? (f a) (f1 a)));
+##| #f; #f1; napply (∀a:A. proofs (eq … (f a) (f1 a)));
 ##| nwhd; #x; #a;
-    napply (f_ok ? ? x ? ? ?); (* QUI!! *)
+    napply (f_ok … x …); (* QUI!! *)
 (*    unfold carr; unfold proofs; simplify;
     apply (refl A)
   | simplify;