- new library/logic/coimplication.ma uses new decompose tactic

[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 28455b520bfe8b31b6e9f75f1e93a9022cedad35..7e8950fee04109475fccadacf922dd94c901039f 100644 (file)
--- a/matita/contribs/CoRN-Decl/transc/RealPowers.ma
+++ b/matita/contribs/CoRN-Decl/transc/RealPowers.ma
@@ -16,7 +16,7 @@
 
 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 $ *)
 
@@ -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
@@ -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".
+inline "cic:/CoRN/transc/RealPowers/Power_Function/J.var" "Power_Function__".
 
-inline "cic:/CoRN/transc/RealPowers/F.var".
+inline "cic:/CoRN/transc/RealPowers/Power_Function/F.var" "Power_Function__".
 
-inline "cic:/CoRN/transc/RealPowers/G.var".
+inline "cic:/CoRN/transc/RealPowers/Power_Function/G.var" "Power_Function__".
 
 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