set "baseuri" "cic:/matita/CoRN-Decl/transc/Trigonometric".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Trigonometric.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
*)
(* UNEXPORTED
-Section Lemmas.
+Section Lemmas
*)
(*#* First, we need a lemma on mappings. *)
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]. *)
*)
(* UNEXPORTED
-Section Sine_of_Sum.
+Section Sine_of_Sum
*)
(*#*
(* 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 *)
inline "cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con".
(* UNEXPORTED
-End Sine_of_Sum.
+End Sine_of_Sum
*)
(* UNEXPORTED
inline "cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con".
(* UNEXPORTED
-End Sine_and_Cosine.
+End Sine_and_Cosine
*)