natural number => Coq natural number

[helm.git] / matita / contribs / CoRN-Decl / transc / RealPowers.ma

diff --git a/matita/contribs/CoRN-Decl/transc/RealPowers.ma b/matita/contribs/CoRN-Decl/transc/RealPowers.ma
index 7e8950fee04109475fccadacf922dd94c901039f..fd081416a06d63a6b8fadb81dd41cb59cf548e21 100644 (file)
--- a/matita/contribs/CoRN-Decl/transc/RealPowers.ma
+++ b/matita/contribs/CoRN-Decl/transc/RealPowers.ma
@@ -141,11 +141,11 @@ on partial functions which preserves continuity.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/transc/RealPowers/Power_Function/J.var" "Power_Function__".
+alias id "J" = "cic:/CoRN/transc/RealPowers/Power_Function/J.var".
 
-inline "cic:/CoRN/transc/RealPowers/Power_Function/F.var" "Power_Function__".
+alias id "F" = "cic:/CoRN/transc/RealPowers/Power_Function/F.var".
 
-inline "cic:/CoRN/transc/RealPowers/Power_Function/G.var" "Power_Function__".
+alias id "G" = "cic:/CoRN/transc/RealPowers/Power_Function/G.var".
 
 inline "cic:/CoRN/transc/RealPowers/FPower.con".