X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=8dfa31342e468a2a45676217e7cbf93e3b3101c1;hb=6d297b12c480352eb2f156ab4515f73921ea2e81;hp=8b1beb7027e18648a6948f178931bcf64915d6da;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma index 8b1beb702..8dfa31342 100644 --- a/helm/software/matita/library/algebra/finite_groups.ma +++ b/helm/software/matita/library/algebra/finite_groups.ma @@ -31,9 +31,6 @@ for @{ 'repr $C $i }. interpretation "Finite_enumerable representation" 'repr C i = (cic:/matita/algebra/finite_groups/repr.con C _ i).*) -notation < "hvbox(|C|)" with precedence 89 -for @{ 'card $C }. - interpretation "Finite_enumerable order" 'card C = (cic:/matita/algebra/finite_groups/order.con C _). @@ -46,7 +43,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"