X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FTrigonometric.ma;h=b4f59a9a8d9ac15ef229640ed9c1e5b8ce0b054d;hb=b7aefa8f362d07bf9042f6879252345e69da07c8;hp=3498c20a84646c654bb8108a9cdb780e2fe423e7;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma b/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
index 3498c20a8..b4f59a9a8 100644
--- a/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
@@ -16,11 +16,11 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/transc/Trigonometric".
 
+include "CoRN.ma".
+
 (* $Id: Trigonometric.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
 
-(* INCLUDE
-TaylorSeries
-*)
+include "transc/TaylorSeries.ma".
 
 (*#* *The Trigonometric Functions
 
@@ -28,26 +28,26 @@ In this section, we explore the properties of the trigonometric functions which
 *)
 
 (* UNEXPORTED
-Section Lemmas.
+Section Lemmas
 *)
 
 (*#* First, we need a lemma on mappings. *)
 
-inline cic:/CoRN/transc/Trigonometric/maps_translation.con.
+inline "cic:/CoRN/transc/Trigonometric/maps_translation.con".
 
 (* UNEXPORTED
-End Lemmas.
+End Lemmas
 *)
 
 (* UNEXPORTED
-Section Sine_and_Cosine.
+Section Sine_and_Cosine
 *)
 
 (*#* Sine, cosine and tangent at [Zero]. *)
 
-inline cic:/CoRN/transc/Trigonometric/Sin_zero.con.
+inline "cic:/CoRN/transc/Trigonometric/Sin_zero.con".
 
-inline cic:/CoRN/transc/Trigonometric/Cos_zero.con.
+inline "cic:/CoRN/transc/Trigonometric/Cos_zero.con".
 
 (* UNEXPORTED
 Hint Resolve Sin_zero Cos_zero: algebra.
@@ -57,7 +57,7 @@ Hint Resolve Sin_zero Cos_zero: algebra.
 Opaque Sine Cosine.
 *)
 
-inline cic:/CoRN/transc/Trigonometric/Tan_zero.con.
+inline "cic:/CoRN/transc/Trigonometric/Tan_zero.con".
 
 (* UNEXPORTED
 Transparent Sine Cosine.
@@ -67,21 +67,21 @@ Transparent Sine Cosine.
 Continuity of sine and cosine are trivial.
 *)
 
-inline cic:/CoRN/transc/Trigonometric/Continuous_Sin.con.
+inline "cic:/CoRN/transc/Trigonometric/Continuous_Sin.con".
 
-inline cic:/CoRN/transc/Trigonometric/Continuous_Cos.con.
+inline "cic:/CoRN/transc/Trigonometric/Continuous_Cos.con".
 
 (*#*
 The rules for the derivative of the sine and cosine function; we begin by proving that their defining sequences can be expressed in terms of one another.
 *)
 
-inline cic:/CoRN/transc/Trigonometric/cos_sin_seq.con.
+inline "cic:/CoRN/transc/Trigonometric/cos_sin_seq.con".
 
-inline cic:/CoRN/transc/Trigonometric/sin_cos_seq.con.
+inline "cic:/CoRN/transc/Trigonometric/sin_cos_seq.con".
 
-inline cic:/CoRN/transc/Trigonometric/Derivative_Sin.con.
+inline "cic:/CoRN/transc/Trigonometric/Derivative_Sin.con".
 
-inline cic:/CoRN/transc/Trigonometric/Derivative_Cos.con.
+inline "cic:/CoRN/transc/Trigonometric/Derivative_Cos.con".
 
 (* UNEXPORTED
 Hint Resolve Derivative_Sin Derivative_Cos: derivate.
@@ -92,7 +92,7 @@ Hint Resolve Continuous_Sin Continuous_Cos: continuous.
 *)
 
 (* UNEXPORTED
-Section Sine_of_Sum.
+Section Sine_of_Sum
 *)
 
 (*#*
@@ -110,13 +110,13 @@ situations).
 
 (* begin hide *)
 
-inline cic:/CoRN/transc/Trigonometric/F.con.
+inline "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F.con" "Sine_and_Cosine__Sine_of_Sum__".
 
-inline cic:/CoRN/transc/Trigonometric/G.con.
+inline "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G.con" "Sine_and_Cosine__Sine_of_Sum__".
 
-inline cic:/CoRN/transc/Trigonometric/F'.con.
+inline "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F'.con" "Sine_and_Cosine__Sine_of_Sum__".
 
-inline cic:/CoRN/transc/Trigonometric/G'.con.
+inline "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G'.con" "Sine_and_Cosine__Sine_of_Sum__".
 
 (* end hide *)
 
@@ -156,7 +156,7 @@ Opaque FAbs.
 Transparent FAbs.
 *)
 
-inline cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_lft.con.
+inline "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_lft.con".
 
 (* UNEXPORTED
 Opaque FAbs.
@@ -190,27 +190,27 @@ Opaque FAbs.
 Transparent FAbs.
 *)
 
-inline cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_rht.con.
+inline "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_rht.con".
 
-inline cic:/CoRN/transc/Trigonometric/Sin_plus_eq.con.
+inline "cic:/CoRN/transc/Trigonometric/Sin_plus_eq.con".
 
-inline cic:/CoRN/transc/Trigonometric/Sin_plus_der_lft.con.
+inline "cic:/CoRN/transc/Trigonometric/Sin_plus_der_lft.con".
 
-inline cic:/CoRN/transc/Trigonometric/Sin_plus_der_rht.con.
+inline "cic:/CoRN/transc/Trigonometric/Sin_plus_der_rht.con".
 
-inline cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con.
+inline "cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con".
 
 (* UNEXPORTED
-End Sine_of_Sum.
+End Sine_of_Sum
 *)
 
 (* UNEXPORTED
 Opaque Sine Cosine.
 *)
 
-inline cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con.
+inline "cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con".
 
 (* UNEXPORTED
-End Sine_and_Cosine.
+End Sine_and_Cosine
 *)