set "baseuri" "cic:/matita/CoRN-Decl/transc/RealPowers".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: RealPowers.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
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
End Power_Function.
*)
+(* NOTATION
+Notation "F {!} G" := (FPower F G) (at level 20).
+*)
+
(* UNEXPORTED
Section More_on_Power_Function.
*)