X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FCalculusTheorems.ma;h=6e43129c362468ec6d1f6c7eb8f0ec935dd7613e;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=57fcf425c0f42fcc59e3f3640b4998437b1a5001;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
index 57fcf425c..6e43129c3 100644
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
@@ -16,15 +16,13 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/ftc/CalculusTheorems".
 
+include "CoRN.ma".
+
 (* $Id: CalculusTheorems.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *)
 
-(* INCLUDE
-Rolle
-*)
+include "ftc/Rolle.ma".
 
-(* INCLUDE
-DiffTactics3
-*)
+include "tactics/DiffTactics3.ma".
 
 (* UNEXPORTED
 Opaque Min Max.
@@ -45,52 +43,52 @@ continuous function commutes with the limit of a numerical sequence
 (sometimes called Heine continuity).
 *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_comm_Lim.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_comm_Lim.con".
 
 (*#*
 This is a tricky result: if [F] is continuous and positive in both [[a,b]]
 and [(b,c]], then it is positive in [[a,c]].
 *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_pos.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/Continuous_imp_pos.con".
 
 (*#*
 Similar results for increasing functions:
 *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues.con".
 
-inline cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues'.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/strict_inc_glues'.con".
 
-inline cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues.con".
 
-inline cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues'.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/strict_dec_glues'.con".
 
 (*#* More on glueing intervals. *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/olor_pos_clor_nonneg.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/olor_pos_clor_nonneg.con".
 
-inline cic:/CoRN/ftc/CalculusTheorems/olor_pos_olcr_nonneg.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/olor_pos_olcr_nonneg.con".
 
-inline cic:/CoRN/ftc/CalculusTheorems/olor_pos_clcr_nonneg.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/olor_pos_clcr_nonneg.con".
 
 (*#*
 Any function that has the null function as its derivative must be constant.
 *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/FConst_prop.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/FConst_prop.con".
 
 (*#* As a corollary, two functions with the same derivative must differ
 by a constant.
 *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/Feq_crit_with_const.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/Feq_crit_with_const.con".
 
 (*#* This yields the following known result: any differential equation
 of the form [f'=g] with initial condition [f(a) [=] b] has a unique solution.
 *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/Feq_criterium.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/Feq_criterium.con".
 
 (*#*
 Finally, a well known result: any function with a (strictly) positive
@@ -99,11 +97,11 @@ quite similar the proofs are completely different, both from the
 formalization and from the mathematical point of view.
 *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less.con".
 
-inline cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_leEq.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_leEq.con".
 
-inline cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less'.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/Derivative_imp_resp_less'.con".
 
 (*#* From these results we can finally prove that exponentiation to a
 real power preserves the less or equal than relation!
@@ -117,7 +115,7 @@ Opaque nring.
 Transparent nring.
 *)
 
-inline cic:/CoRN/ftc/CalculusTheorems/nexp_resp_leEq_odd.con.
+inline "cic:/CoRN/ftc/CalculusTheorems/nexp_resp_leEq_odd.con".
 
 (* UNEXPORTED
 End Various_Theorems.