...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / transc / SinCos.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/transc/SinCos.mma b/helm/software/matita/contribs/CoRN-Procedural/transc/SinCos.mma
index 3ff87c6c6d44301404a9e02e5eec175cc5ced9b0..149ff39a639aba390033fd8b762f468012e2f607 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/transc/SinCos.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/transc/SinCos.mma
@@ -30,19 +30,19 @@ Opaque Sine Cosine.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/F.con" "Sum_and_so_on__".
+inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/F.con" "Sum_and_so_on__" as definition.
 
-inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/G.con" "Sum_and_so_on__".
+inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/G.con" "Sum_and_so_on__" as definition.
 
-inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/F'.con" "Sum_and_so_on__".
+inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/F'.con" "Sum_and_so_on__" as definition.
 
-inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/G'.con" "Sum_and_so_on__".
+inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/G'.con" "Sum_and_so_on__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/transc/SinCos/Sin_plus.con".
+inline procedural "cic:/CoRN/transc/SinCos/Sin_plus.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Cos_plus.con".
+inline procedural "cic:/CoRN/transc/SinCos/Cos_plus.con" as lemma.
 
 (* UNEXPORTED
 Opaque Sine Cosine.
@@ -54,7 +54,7 @@ Hint Resolve Cos_plus Sin_plus: algebra.
 
 (*#* As a corollary we get the rule for the tangent of the sum. *)
 
-inline procedural "cic:/CoRN/transc/SinCos/Tan_plus.con".
+inline procedural "cic:/CoRN/transc/SinCos/Tan_plus.con" as lemma.
 
 (* UNEXPORTED
 Transparent Sine Cosine.
@@ -62,9 +62,9 @@ Transparent Sine Cosine.
 
 (*#* Sine, cosine and tangent of [[--]x]. *)
 
-inline procedural "cic:/CoRN/transc/SinCos/Cos_inv.con".
+inline procedural "cic:/CoRN/transc/SinCos/Cos_inv.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Sin_inv.con".
+inline procedural "cic:/CoRN/transc/SinCos/Sin_inv.con" as lemma.
 
 (* UNEXPORTED
 Opaque Sine Cosine.
@@ -74,7 +74,7 @@ Opaque Sine Cosine.
 Hint Resolve Cos_inv Sin_inv: algebra.
 *)
 
-inline procedural "cic:/CoRN/transc/SinCos/Tan_inv.con".
+inline procedural "cic:/CoRN/transc/SinCos/Tan_inv.con" as lemma.
 
 (* UNEXPORTED
 Transparent Sine Cosine.
@@ -88,7 +88,7 @@ The fundamental formulas of trigonometry: $\cos(x)^2+\sin(x)^2=1$#cos(x)<sup>2</
 Hint Resolve Cos_zero: algebra.
 *)
 
-inline procedural "cic:/CoRN/transc/SinCos/FFT.con".
+inline procedural "cic:/CoRN/transc/SinCos/FFT.con" as theorem.
 
 (* UNEXPORTED
 Opaque Sine Cosine.
@@ -98,7 +98,7 @@ Opaque Sine Cosine.
 Hint Resolve FFT: algebra.
 *)
 
-inline procedural "cic:/CoRN/transc/SinCos/FFT'.con".
+inline procedural "cic:/CoRN/transc/SinCos/FFT'.con" as lemma.
 
 (* UNEXPORTED
 End Sum_and_so_on
@@ -132,37 +132,37 @@ We now prove most of the usual trigonometric (in)equalities.
 Sine, cosine and tangent are strongly extensional and well defined.
 *)
 
-inline procedural "cic:/CoRN/transc/SinCos/Sin_strext.con".
+inline procedural "cic:/CoRN/transc/SinCos/Sin_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Cos_strext.con".
+inline procedural "cic:/CoRN/transc/SinCos/Cos_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Tan_strext.con".
+inline procedural "cic:/CoRN/transc/SinCos/Tan_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Sin_wd.con".
+inline procedural "cic:/CoRN/transc/SinCos/Sin_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Cos_wd.con".
+inline procedural "cic:/CoRN/transc/SinCos/Cos_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Tan_wd.con".
+inline procedural "cic:/CoRN/transc/SinCos/Tan_wd.con" as lemma.
 
 (*#*
 The sine and cosine produce values in [[-1,1]].
 *)
 
-inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Sin_leEq_One.con".
+inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Sin_leEq_One.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Cos_leEq_One.con".
+inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Cos_leEq_One.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Sin_leEq_One.con".
+inline procedural "cic:/CoRN/transc/SinCos/Sin_leEq_One.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/Cos_leEq_One.con".
+inline procedural "cic:/CoRN/transc/SinCos/Cos_leEq_One.con" as lemma.
 
 (*#*
 If the cosine is positive then the sine is in [(-1,1)].
 *)
 
-inline procedural "cic:/CoRN/transc/SinCos/Sin_less_One.con".
+inline procedural "cic:/CoRN/transc/SinCos/Sin_less_One.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Sin_less_One.con".
+inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Sin_less_One.con" as lemma.
 
 (* UNEXPORTED
 End Basic_Properties