X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=d3f5cf27294cba1f71251cf9b9b5f46edffd8277;hb=59c1da7b30cc49916a636682556ed1b9532cd146;hp=766f9a6a73e457ae1d6e9630c9661b8bacec8eb5;hpb=9e291b4d0a99118cd0a1c5540ef00c25ca37a56d;p=helm.git diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma index 766f9a6a7..d3f5cf272 100644 --- a/helm/software/matita/library/algebra/finite_groups.ma +++ b/helm/software/matita/library/algebra/finite_groups.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/algebra/finite_groups/". - include "algebra/groups.ma". record finite_enumerable (T:Type) : Type≝ @@ -48,7 +46,7 @@ interpretation "Finite_enumerable representation" 'repr S i = (cic:/matita/algebra/finite_groups/repr.con S (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i). -notation "hvbox(ι e)" with precedence 60 +notation "hvbox(\iota e)" with precedence 60 for @{ 'index_of_finite_enumerable_semigroup $e }. interpretation "Index_of_finite_enumerable representation"