X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FSinCos.ma;h=314d0f5fa686496b7232784a91871434ce2fd2eb;hb=5e01cba364607e7937aec2e359c34f049bb0f108;hp=b52f1f30041dd4dbec5828d59b22044344fb33e3;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma b/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma
index b52f1f300..314d0f5fa 100644
--- a/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma
@@ -16,14 +16,14 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/transc/SinCos".
 
+include "CoRN.ma".
+
 (* $Id: SinCos.v,v 1.6 2004/04/23 10:01:08 lcf Exp $ *)
 
-(* INCLUDE
-Trigonometric
-*)
+include "transc/Trigonometric.ma".
 
 (* UNEXPORTED
-Section Sum_and_so_on.
+Section Sum_and_so_on
 *)
 
 (* UNEXPORTED
@@ -32,19 +32,19 @@ Opaque Sine Cosine.
 
 (* begin hide *)
 
-inline cic:/CoRN/transc/SinCos/F.con.
+inline "cic:/CoRN/transc/SinCos/Sum_and_so_on/F.con" "Sum_and_so_on__".
 
-inline cic:/CoRN/transc/SinCos/G.con.
+inline "cic:/CoRN/transc/SinCos/Sum_and_so_on/G.con" "Sum_and_so_on__".
 
-inline cic:/CoRN/transc/SinCos/F'.con.
+inline "cic:/CoRN/transc/SinCos/Sum_and_so_on/F'.con" "Sum_and_so_on__".
 
-inline cic:/CoRN/transc/SinCos/G'.con.
+inline "cic:/CoRN/transc/SinCos/Sum_and_so_on/G'.con" "Sum_and_so_on__".
 
 (* end hide *)
 
-inline cic:/CoRN/transc/SinCos/Sin_plus.con.
+inline "cic:/CoRN/transc/SinCos/Sin_plus.con".
 
-inline cic:/CoRN/transc/SinCos/Cos_plus.con.
+inline "cic:/CoRN/transc/SinCos/Cos_plus.con".
 
 (* UNEXPORTED
 Opaque Sine Cosine.
@@ -56,7 +56,7 @@ Hint Resolve Cos_plus Sin_plus: algebra.
 
 (*#* As a corollary we get the rule for the tangent of the sum. *)
 
-inline cic:/CoRN/transc/SinCos/Tan_plus.con.
+inline "cic:/CoRN/transc/SinCos/Tan_plus.con".
 
 (* UNEXPORTED
 Transparent Sine Cosine.
@@ -64,9 +64,9 @@ Transparent Sine Cosine.
 
 (*#* Sine, cosine and tangent of [[--]x]. *)
 
-inline cic:/CoRN/transc/SinCos/Cos_inv.con.
+inline "cic:/CoRN/transc/SinCos/Cos_inv.con".
 
-inline cic:/CoRN/transc/SinCos/Sin_inv.con.
+inline "cic:/CoRN/transc/SinCos/Sin_inv.con".
 
 (* UNEXPORTED
 Opaque Sine Cosine.
@@ -76,7 +76,7 @@ Opaque Sine Cosine.
 Hint Resolve Cos_inv Sin_inv: algebra.
 *)
 
-inline cic:/CoRN/transc/SinCos/Tan_inv.con.
+inline "cic:/CoRN/transc/SinCos/Tan_inv.con".
 
 (* UNEXPORTED
 Transparent Sine Cosine.
@@ -90,7 +90,7 @@ The fundamental formulas of trigonometry: $\cos(x)^2+\sin(x)^2=1$#cos(x)<sup>2</
 Hint Resolve Cos_zero: algebra.
 *)
 
-inline cic:/CoRN/transc/SinCos/FFT.con.
+inline "cic:/CoRN/transc/SinCos/FFT.con".
 
 (* UNEXPORTED
 Opaque Sine Cosine.
@@ -100,10 +100,10 @@ Opaque Sine Cosine.
 Hint Resolve FFT: algebra.
 *)
 
-inline cic:/CoRN/transc/SinCos/FFT'.con.
+inline "cic:/CoRN/transc/SinCos/FFT'.con".
 
 (* UNEXPORTED
-End Sum_and_so_on.
+End Sum_and_so_on
 *)
 
 (* UNEXPORTED
@@ -124,7 +124,7 @@ Opaque Min Sine Cosine.
 *)
 
 (* UNEXPORTED
-Section Basic_Properties.
+Section Basic_Properties
 *)
 
 (*#* **Basic properties
@@ -134,40 +134,40 @@ We now prove most of the usual trigonometric (in)equalities.
 Sine, cosine and tangent are strongly extensional and well defined.
 *)
 
-inline cic:/CoRN/transc/SinCos/Sin_strext.con.
+inline "cic:/CoRN/transc/SinCos/Sin_strext.con".
 
-inline cic:/CoRN/transc/SinCos/Cos_strext.con.
+inline "cic:/CoRN/transc/SinCos/Cos_strext.con".
 
-inline cic:/CoRN/transc/SinCos/Tan_strext.con.
+inline "cic:/CoRN/transc/SinCos/Tan_strext.con".
 
-inline cic:/CoRN/transc/SinCos/Sin_wd.con.
+inline "cic:/CoRN/transc/SinCos/Sin_wd.con".
 
-inline cic:/CoRN/transc/SinCos/Cos_wd.con.
+inline "cic:/CoRN/transc/SinCos/Cos_wd.con".
 
-inline cic:/CoRN/transc/SinCos/Tan_wd.con.
+inline "cic:/CoRN/transc/SinCos/Tan_wd.con".
 
 (*#*
 The sine and cosine produce values in [[-1,1]].
 *)
 
-inline cic:/CoRN/transc/SinCos/AbsIR_Sin_leEq_One.con.
+inline "cic:/CoRN/transc/SinCos/AbsIR_Sin_leEq_One.con".
 
-inline cic:/CoRN/transc/SinCos/AbsIR_Cos_leEq_One.con.
+inline "cic:/CoRN/transc/SinCos/AbsIR_Cos_leEq_One.con".
 
-inline cic:/CoRN/transc/SinCos/Sin_leEq_One.con.
+inline "cic:/CoRN/transc/SinCos/Sin_leEq_One.con".
 
-inline cic:/CoRN/transc/SinCos/Cos_leEq_One.con.
+inline "cic:/CoRN/transc/SinCos/Cos_leEq_One.con".
 
 (*#*
 If the cosine is positive then the sine is in [(-1,1)].
 *)
 
-inline cic:/CoRN/transc/SinCos/Sin_less_One.con.
+inline "cic:/CoRN/transc/SinCos/Sin_less_One.con".
 
-inline cic:/CoRN/transc/SinCos/AbsIR_Sin_less_One.con.
+inline "cic:/CoRN/transc/SinCos/AbsIR_Sin_less_One.con".
 
 (* UNEXPORTED
-End Basic_Properties.
+End Basic_Properties
 *)
 
 (* UNEXPORTED