X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCSums.ma;h=3930cbf9febd05b374bad1b227d8fee8c85f6638;hb=842e243be954d67360788d08701289f3237c2699;hp=c90312746f3ca716307189216a9b55c439db2455;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma index c90312746..3930cbf9f 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma @@ -42,7 +42,7 @@ include "algebra/CAbGroups.ma". Section Sums *) -inline "cic:/CoRN/algebra/CSums/Sums/G.var" "Sums__". +alias id "G" = "cic:/CoRN/algebra/CSums/Sums/G.var". (* Sum1 and Sum use subtraction *) @@ -219,7 +219,7 @@ often referred to as ``Mengolli Sums''. Section More_Sums *) -inline "cic:/CoRN/algebra/CSums/More_Sums/G.var" "More_Sums__". +alias id "G" = "cic:/CoRN/algebra/CSums/More_Sums/G.var". inline "cic:/CoRN/algebra/CSums/Mengolli_Sum.con".