fix

[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 5c4f4cbddcfb04e3ecec67b724e872c7a780461e..015d267fe3b99331278d39fc79fcb3e86d0170d7 100644 (file)
--- a/matita/contribs/CoRN-Decl/transc/RealPowers.ma
+++ b/matita/contribs/CoRN-Decl/transc/RealPowers.ma
@@ -41,6 +41,10 @@ $x^y=e^{y\times\log(x)}$#x<sup>y</sup>=e<sup>y*log(x)</sup>#, 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
@@ -153,6 +157,10 @@ inline "cic:/CoRN/transc/RealPowers/Continuous_power.con".
 End Power_Function.
 *)
 
+(* NOTATION
+Notation "F {!} G" := (FPower F G) (at level 20).
+*)
+
 (* UNEXPORTED
 Section More_on_Power_Function.
 *)