]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma
- transcript: patched to generate aliases instead of inlined variables
[helm.git] / helm / software / matita / contribs / CoRN-Decl / algebra / CSums.ma
index c90312746f3ca716307189216a9b55c439db2455..3930cbf9febd05b374bad1b227d8fee8c85f6638 100644 (file)
@@ -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".