freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma b/helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
index 015d267fe3b99331278d39fc79fcb3e86d0170d7..fd081416a06d63a6b8fadb81dd41cb59cf548e21 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
@@ -129,7 +129,7 @@ Hint Resolve power_div: algebra.
 *)
 
 (* UNEXPORTED
-Section Power_Function.
+Section Power_Function
 *)
 
 (*#* **Power Function
@@ -141,11 +141,11 @@ on partial functions which preserves continuity.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/transc/RealPowers/J.var".
+alias id "J" = "cic:/CoRN/transc/RealPowers/Power_Function/J.var".
 
-inline "cic:/CoRN/transc/RealPowers/F.var".
+alias id "F" = "cic:/CoRN/transc/RealPowers/Power_Function/F.var".
 
-inline "cic:/CoRN/transc/RealPowers/G.var".
+alias id "G" = "cic:/CoRN/transc/RealPowers/Power_Function/G.var".
 
 inline "cic:/CoRN/transc/RealPowers/FPower.con".
 
@@ -154,7 +154,7 @@ inline "cic:/CoRN/transc/RealPowers/FPower_domain.con".
 inline "cic:/CoRN/transc/RealPowers/Continuous_power.con".
 
 (* UNEXPORTED
-End Power_Function.
+End Power_Function
 *)
 
 (* NOTATION
@@ -162,7 +162,7 @@ Notation "F {!} G" := (FPower F G) (at level 20).
 *)
 
 (* UNEXPORTED
-Section More_on_Power_Function.
+Section More_on_Power_Function
 *)
 
 (* UNEXPORTED
@@ -188,7 +188,7 @@ inline "cic:/CoRN/transc/RealPowers/Derivative_power.con".
 inline "cic:/CoRN/transc/RealPowers/Diffble_power.con".
 
 (* UNEXPORTED
-End More_on_Power_Function.
+End More_on_Power_Function
 *)
 
 (* UNEXPORTED