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=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..8dfa31342 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≝
@@ -33,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 _).
 
@@ -48,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"