X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=d3f5cf27294cba1f71251cf9b9b5f46edffd8277;hb=7ce9eb0e973e414c988b416d118efe860516e275;hp=0c7bd0b641914886a1ad659291da5b12eaff545c;hpb=af130d273b6be7fbcc2fb2504f3b28ef8fa2344f;p=helm.git

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 0c7bd0b64..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"
@@ -93,6 +91,7 @@ elim n;
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
+          unfold f' in H5;
           clear f';
           elim H5;
           clear H5;
@@ -161,6 +160,7 @@ elim n;
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
+          unfold f' in H5;
           clear f';
           elim H5;
           clear H5;
@@ -395,6 +395,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
       assumption
     ]
   | intros;
+    unfold f;
     apply index_of_sur
   ] 
 ].