- 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 26a378354dbe62d3cf1006353d0ac239b360a010..7e8950fee04109475fccadacf922dd94c901039f 100644 (file)
--- a/matita/contribs/CoRN-Decl/transc/RealPowers.ma
+++ b/matita/contribs/CoRN-Decl/transc/RealPowers.ma
@@ -16,15 +16,15 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/transc/RealPowers".
 
+include "CoRN.ma".
+
 (* $Id: RealPowers.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
 
 (*#* printing [!] %\ensuremath{\hat{\ }}% #^# *)
 
 (*#* printing {!} %\ensuremath{\hat{\ }}% #^# *)
 
-(* INCLUDE
-Exponential
-*)
+include "transc/Exponential.ma".
 
 (* UNEXPORTED
 Opaque Expon.
@@ -39,7 +39,11 @@ $x^y=e^{y\times\log(x)}$#x<sup>y</sup>=e<sup>y*log(x)</sup>#, whenever
 [x [>] 0], inspired by the rules for manipulating these expressions.
 *)
 
-inline cic:/CoRN/transc/RealPowers/power.con.
+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
@@ -48,29 +52,29 @@ still has all the good properties of that operation; when [x [=] e] it
 coincides with the exponential function.
 *)
 
-inline cic:/CoRN/transc/RealPowers/power_wd.con.
+inline "cic:/CoRN/transc/RealPowers/power_wd.con".
 
-inline cic:/CoRN/transc/RealPowers/power_strext.con.
+inline "cic:/CoRN/transc/RealPowers/power_strext.con".
 
-inline cic:/CoRN/transc/RealPowers/power_plus.con.
+inline "cic:/CoRN/transc/RealPowers/power_plus.con".
 
-inline cic:/CoRN/transc/RealPowers/power_inv.con.
+inline "cic:/CoRN/transc/RealPowers/power_inv.con".
 
 (* UNEXPORTED
 Hint Resolve power_wd power_plus power_inv: algebra.
 *)
 
-inline cic:/CoRN/transc/RealPowers/power_minus.con.
+inline "cic:/CoRN/transc/RealPowers/power_minus.con".
 
-inline cic:/CoRN/transc/RealPowers/power_nat.con.
+inline "cic:/CoRN/transc/RealPowers/power_nat.con".
 
 (* UNEXPORTED
 Hint Resolve power_minus power_nat: algebra.
 *)
 
-inline cic:/CoRN/transc/RealPowers/power_zero.con.
+inline "cic:/CoRN/transc/RealPowers/power_zero.con".
 
-inline cic:/CoRN/transc/RealPowers/power_one.con.
+inline "cic:/CoRN/transc/RealPowers/power_one.con".
 
 (* UNEXPORTED
 Hint Resolve power_zero power_one: algebra.
@@ -80,52 +84,52 @@ Hint Resolve power_zero power_one: algebra.
 Opaque nexp_op.
 *)
 
-inline cic:/CoRN/transc/RealPowers/power_int.con.
+inline "cic:/CoRN/transc/RealPowers/power_int.con".
 
 (* UNEXPORTED
 Hint Resolve power_int: algebra.
 *)
 
-inline cic:/CoRN/transc/RealPowers/Exp_power.con.
+inline "cic:/CoRN/transc/RealPowers/Exp_power.con".
 
-inline cic:/CoRN/transc/RealPowers/mult_power.con.
+inline "cic:/CoRN/transc/RealPowers/mult_power.con".
 
-inline cic:/CoRN/transc/RealPowers/recip_power.con.
+inline "cic:/CoRN/transc/RealPowers/recip_power.con".
 
 (* UNEXPORTED
 Hint Resolve Exp_power mult_power recip_power: algebra.
 *)
 
-inline cic:/CoRN/transc/RealPowers/div_power.con.
+inline "cic:/CoRN/transc/RealPowers/div_power.con".
 
 (* UNEXPORTED
 Hint Resolve div_power: algebra.
 *)
 
-inline cic:/CoRN/transc/RealPowers/power_ap_zero.con.
+inline "cic:/CoRN/transc/RealPowers/power_ap_zero.con".
 
-inline cic:/CoRN/transc/RealPowers/power_mult.con.
+inline "cic:/CoRN/transc/RealPowers/power_mult.con".
 
-inline cic:/CoRN/transc/RealPowers/power_pos.con.
+inline "cic:/CoRN/transc/RealPowers/power_pos.con".
 
 (* UNEXPORTED
 Hint Resolve power_mult: algebra.
 *)
 
-inline cic:/CoRN/transc/RealPowers/power_recip.con.
+inline "cic:/CoRN/transc/RealPowers/power_recip.con".
 
 (* UNEXPORTED
 Hint Resolve power_recip: algebra.
 *)
 
-inline cic:/CoRN/transc/RealPowers/power_div.con.
+inline "cic:/CoRN/transc/RealPowers/power_div.con".
 
 (* UNEXPORTED
 Hint Resolve power_div: algebra.
 *)
 
 (* UNEXPORTED
-Section Power_Function.
+Section Power_Function
 *)
 
 (*#* **Power Function
@@ -137,24 +141,28 @@ 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.
+inline "cic:/CoRN/transc/RealPowers/FPower.con".
 
-inline cic:/CoRN/transc/RealPowers/FPower_domain.con.
+inline "cic:/CoRN/transc/RealPowers/FPower_domain.con".
 
-inline cic:/CoRN/transc/RealPowers/Continuous_power.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
@@ -163,7 +171,7 @@ Opaque Expon Logarithm.
 
 (*#* From global continuity we can obviously get local continuity: *)
 
-inline cic:/CoRN/transc/RealPowers/continuous_I_power.con.
+inline "cic:/CoRN/transc/RealPowers/continuous_I_power.con".
 
 (*#* The rule for differentiation is a must. *)
 
@@ -175,12 +183,12 @@ Transparent Logarithm.
 Opaque Logarithm.
 *)
 
-inline cic:/CoRN/transc/RealPowers/Derivative_power.con.
+inline "cic:/CoRN/transc/RealPowers/Derivative_power.con".
 
-inline cic:/CoRN/transc/RealPowers/Diffble_power.con.
+inline "cic:/CoRN/transc/RealPowers/Diffble_power.con".
 
 (* UNEXPORTED
-End More_on_Power_Function.
+End More_on_Power_Function
 *)
 
 (* UNEXPORTED