X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=6da0a7256b0eb0517ca203228041d58a4e6ed72e;hb=6daa2cc113783aaba53d82c47fe7107988d76e11;hp=36573a8a7d0598217d5cae8cb8c00c9d01ffc8b4;hpb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;p=helm.git diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma index 36573a8a7..6da0a7256 100644 --- a/helm/software/matita/library/algebra/finite_groups.ma +++ b/helm/software/matita/library/algebra/finite_groups.ma @@ -29,9 +29,9 @@ for @{ 'repr $C $i }. (* CSC: multiple interpretations in the same file are not considered in the right order -interpretation "Finite_enumerable representation" 'repr C i = (repr C _ i).*) +interpretation "Finite_enumerable representation" 'repr C i = (repr C ? i).*) -interpretation "Finite_enumerable order" 'card C = (order C _). +interpretation "Finite_enumerable order" 'card C = (order C ?). record finite_enumerable_SemiGroup : Type≝ { semigroup:> SemiGroup; @@ -47,7 +47,7 @@ for @{ 'index_of_finite_enumerable_semigroup $e }. interpretation "Index_of_finite_enumerable representation" 'index_of_finite_enumerable_semigroup e = - (index_of _ (is_finite_enumerable _) e). + (index_of ? (is_finite_enumerable ?) e). (* several definitions/theorems to be moved somewhere else *)