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
*)
(* UNEXPORTED
-Section Power_Function.
+Section Power_Function
*)
(*#* **Power Function
%\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".
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
inline "cic:/CoRN/transc/RealPowers/Diffble_power.con".
(* UNEXPORTED
-End More_on_Power_Function.
+End More_on_Power_Function
*)
(* UNEXPORTED