X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FRealPowers.ma;h=fd081416a06d63a6b8fadb81dd41cb59cf548e21;hb=5b8db2a058d6a86d7d87db190e6e00e444fe7a45;hp=5c4f4cbddcfb04e3ecec67b724e872c7a780461e;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;p=helm.git
diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma b/helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
index 5c4f4cbdd..fd081416a 100644
--- a/helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
@@ -41,6 +41,10 @@ $x^y=e^{y\times\log(x)}$#xy=ey*log(x)#, whenever
inline "cic:/CoRN/transc/RealPowers/power.con".
+(* NOTATION
+Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
+*)
+
(*#*
This definition yields a well defined, strongly extensional function
which extends the algebraic exponentiation to an integer power and
@@ -125,7 +129,7 @@ Hint Resolve power_div: algebra.
*)
(* UNEXPORTED
-Section Power_Function.
+Section Power_Function
*)
(*#* **Power Function
@@ -137,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".
@@ -150,11 +154,15 @@ inline "cic:/CoRN/transc/RealPowers/FPower_domain.con".
inline "cic:/CoRN/transc/RealPowers/Continuous_power.con".
(* UNEXPORTED
-End Power_Function.
+End Power_Function
+*)
+
+(* NOTATION
+Notation "F {!} G" := (FPower F G) (at level 20).
*)
(* UNEXPORTED
-Section More_on_Power_Function.
+Section More_on_Power_Function
*)
(* UNEXPORTED
@@ -180,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