X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Fgroups.ma;h=9ab695239665e8418d6279f8f1609334e7ddada1;hb=32d8d8d419e0b910435da275361bb55d49bc43a9;hp=6cb99481241e95a8c945902816d8832e5d8094c9;hpb=ee3f8d6fa92b051394a2ff7c71c03ac33a05182b;p=helm.git

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index 6cb994812..9ab695239 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -190,7 +190,7 @@ for @{ 'subgroupimage $H $x }.
 
 interpretation "Subgroup image" 'subgroupimage H x =
  (cic:/matita/algebra/groups/image.con _ _
-   (cic:/matita/algebra/groups/morphism_of_subgroup.con _ H) x).
+   (cic:/matita/algebra/groups/morphism_OF_subgroup.con _ H) x).
 
 definition member_of_subgroup ≝
  λG.λH:subgroup G.λx:G.∃y.x=y \sub H.
@@ -296,7 +296,7 @@ qed.
 
 (*CSC: here the coercion Type_of_Group cannot be omitted. Why? *)
 theorem in_x_mk_left_coset_x_H:
- ∀G.∀x:Type_of_Group G.∀H:subgroup G.x ∈ (x*H).
+ ∀G.∀x:Type_OF_Group G.∀H:subgroup G.x ∈ (x*H).
 intros;
 simplify;
 apply (ex_intro ? ? 1);