X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2Fiso_CReals.ma;h=40fc12b205d9f08f3faf97ac63d29de5329c35f5;hb=1d8389a897e804825909cc84640e0d5c5f58e543;hp=c7e115dd91ccbe978666ab8e74f8bff572f9ab14;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma b/helm/software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma
index c7e115dd9..40fc12b20 100644
--- a/helm/software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma
@@ -61,9 +61,9 @@ inline "cic:/CoRN/reals/iso_CReals/G_pres_mult.con".
 Section Concrete_iso_between_Creals
 *)
 
-inline "cic:/CoRN/reals/iso_CReals/Concrete_iso_between_Creals/R1.var" "Concrete_iso_between_Creals__".
+alias id "R1" = "cic:/CoRN/reals/iso_CReals/Concrete_iso_between_Creals/R1.var".
 
-inline "cic:/CoRN/reals/iso_CReals/Concrete_iso_between_Creals/R2.var" "Concrete_iso_between_Creals__".
+alias id "R2" = "cic:/CoRN/reals/iso_CReals/Concrete_iso_between_Creals/R2.var".
 
 inline "cic:/CoRN/reals/iso_CReals/image_Cauchy12.con".