From a6c0e26692598b528ad9a697fa580ba915962d42 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 10 Jul 2006 17:07:49 +0000 Subject: [PATCH] renamed the coercion --- helm/software/matita/library/algebra/groups.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma index 6cb994812..884e0c582 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. -- 2.39.2