X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FCalculusTheorems.ma;h=37510497572b983fe86912bdbc592fd981b6d3f7;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=57fcf425c0f42fcc59e3f3640b4998437b1a5001;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma b/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
index 57fcf425c..375104975 100644
--- a/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
+++ b/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
@@ -16,22 +16,20 @@
 
 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.
 *)
 
 (* UNEXPORTED
-Section Various_Theorems.
+Section Various_Theorems
 *)
 
 (*#* *Calculus Theorems
@@ -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,9 +115,9 @@ 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.
+End Various_Theorems
 *)