Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/transc/Trigonometric.mma b/helm/software/matita/contribs/CoRN-Procedural/transc/Trigonometric.mma
index 8c20f075d3467d3346a35399905e5ca413a6318e..7308dd1e2309929817fe2c484823ecc7616ba043 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/transc/Trigonometric.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/transc/Trigonometric.mma
@@ -31,7 +31,7 @@ Section Lemmas
 
 (*#* First, we need a lemma on mappings. *)
 
-inline procedural "cic:/CoRN/transc/Trigonometric/maps_translation.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/maps_translation.con" as lemma.
 
 (* UNEXPORTED
 End Lemmas
@@ -43,9 +43,9 @@ Section Sine_and_Cosine
 
 (*#* Sine, cosine and tangent at [Zero]. *)
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sin_zero.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sin_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Cos_zero.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Cos_zero.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Sin_zero Cos_zero: algebra.
@@ -55,7 +55,7 @@ Hint Resolve Sin_zero Cos_zero: algebra.
 Opaque Sine Cosine.
 *)
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Tan_zero.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Tan_zero.con" as lemma.
 
 (* UNEXPORTED
 Transparent Sine Cosine.
@@ -65,21 +65,21 @@ Transparent Sine Cosine.
 Continuity of sine and cosine are trivial.
 *)
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Continuous_Sin.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Continuous_Sin.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Continuous_Cos.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Continuous_Cos.con" as lemma.
 
 (*#*
 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 procedural "cic:/CoRN/transc/Trigonometric/cos_sin_seq.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/cos_sin_seq.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/sin_cos_seq.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/sin_cos_seq.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Derivative_Sin.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Derivative_Sin.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Derivative_Cos.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Derivative_Cos.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Derivative_Sin Derivative_Cos: derivate.
@@ -108,13 +108,13 @@ situations).
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F.con" "Sine_and_Cosine__Sine_of_Sum__".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G.con" "Sine_and_Cosine__Sine_of_Sum__".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F'.con" "Sine_and_Cosine__Sine_of_Sum__".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F'.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G'.con" "Sine_and_Cosine__Sine_of_Sum__".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G'.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
 
 (* end hide *)
 
@@ -154,7 +154,7 @@ Opaque FAbs.
 Transparent FAbs.
 *)
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_lft.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_lft.con" as lemma.
 
 (* UNEXPORTED
 Opaque FAbs.
@@ -188,15 +188,15 @@ Opaque FAbs.
 Transparent FAbs.
 *)
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_rht.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_rht.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_eq.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_eq.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_der_lft.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_der_lft.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_der_rht.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_der_rht.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con" as lemma.
 
 (* UNEXPORTED
 End Sine_of_Sum
@@ -206,7 +206,7 @@ End Sine_of_Sum
 Opaque Sine Cosine.
 *)
 
-inline procedural "cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con".
+inline procedural "cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con" as lemma.
 
 (* UNEXPORTED
 End Sine_and_Cosine