X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=36573a8a7d0598217d5cae8cb8c00c9d01ffc8b4;hb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;hp=8dfa31342e468a2a45676217e7cbf93e3b3101c1;hpb=187b433512cba119f84a476395e9df98136b1a56;p=helm.git

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 8dfa31342..36573a8a7 100644
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "algebra/groups.ma".
+include "nat/relevant_equations.ma".
 
 record finite_enumerable (T:Type) : Type≝
  { order: nat;
@@ -28,11 +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 =
- (cic:/matita/algebra/finite_groups/repr.con C _ i).*)
+interpretation "Finite_enumerable representation" 'repr C i = (repr C _ i).*)
  
-interpretation "Finite_enumerable order" 'card C =
- (cic:/matita/algebra/finite_groups/order.con C _).
+interpretation "Finite_enumerable order" 'card C = (order C _).
 
 record finite_enumerable_SemiGroup : Type≝
  { semigroup:> SemiGroup;
@@ -40,8 +39,7 @@ record finite_enumerable_SemiGroup : Type≝
  }.
 
 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).
+ (repr S (is_finite_enumerable S) i).
 
 notation "hvbox(\iota e)" with precedence 60
 for @{ 'index_of_finite_enumerable_semigroup $e }.
@@ -49,8 +47,7 @@ for @{ 'index_of_finite_enumerable_semigroup $e }.
 interpretation "Index_of_finite_enumerable representation"
  'index_of_finite_enumerable_semigroup e
 =
- (cic:/matita/algebra/finite_groups/index_of.con _
-  (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e).
+ (index_of _ (is_finite_enumerable _) e).
 
 
 (* several definitions/theorems to be moved somewhere else *)
@@ -248,8 +245,7 @@ elim n;
       [ apply (H1 ? ? ? ? Hcut);
         apply le_S;
         assumption
-      | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con".
-apply eq_pred_to_eq;
+      | apply eq_pred_to_eq;
         [ apply (ltn_to_ltO ? ? H7)
         | apply (ltn_to_ltO ? ? H6)
         | assumption