added some notation

[helm.git] / helm / software / matita / contribs / CoRN-Decl / complex / CComplex.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma b/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma
index c28c05ed188de7226c8a261799895f053b6965c4..de4d83dbead3cb7b7aed077bd031d2f8330c31ac 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/complex/CComplex".
 
-include "CoRN_notation.ma".
+include "CoRN.ma".
 
 (* $Id: CComplex.v,v 1.8 2004/04/23 10:00:55 lcf Exp $ *)
 
@@ -41,7 +41,7 @@ include "reals/NRootIR.ma".
 *)
 
 (* UNEXPORTED
-Section Complex_Numbers.
+Section Complex_Numbers
 *)
 
 inline "cic:/CoRN/complex/CComplex/CC_set.ind".
@@ -189,19 +189,27 @@ inline "cic:/CoRN/complex/CComplex/AbsCC.con".
 inline "cic:/CoRN/complex/CComplex/TwoCC_ap_zero.con".
 
 (* UNEXPORTED
-End Complex_Numbers.
+End Complex_Numbers
 *)
 
 (* begin hide *)
 
+(* NOTATION
+Notation CCX := (cpoly_cring CC).
+*)
+
 (* end hide *)
 
 inline "cic:/CoRN/complex/CComplex/II.con".
 
+(* NOTATION
+Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
+*)
+
 (*#* ** Properties of [II] *)
 
 (* UNEXPORTED
-Section I_properties.
+Section I_properties
 *)
 
 inline "cic:/CoRN/complex/CComplex/I_square.con".
@@ -243,7 +251,7 @@ inline "cic:/CoRN/complex/CComplex/Im_resp_inv.con".
 inline "cic:/CoRN/complex/CComplex/cc_calculate_square.con".
 
 (* UNEXPORTED
-End I_properties.
+End I_properties
 *)
 
 (* UNEXPORTED
@@ -258,7 +266,7 @@ Hint Resolve I_wd Re_wd Im_wd: algebra_c.
 (*#* ** Properties of conjugation *)
 
 (* UNEXPORTED
-Section Conj_properties.
+Section Conj_properties
 *)
 
 inline "cic:/CoRN/complex/CComplex/CC_conj_plus.con".
@@ -284,7 +292,7 @@ Hint Resolve CC_conj_one: algebra.
 inline "cic:/CoRN/complex/CComplex/CC_conj_nexp.con".
 
 (* UNEXPORTED
-End Conj_properties.
+End Conj_properties
 *)
 
 (* UNEXPORTED
@@ -295,7 +303,7 @@ Hint Resolve CC_conj_plus CC_conj_mult CC_conj_nexp CC_conj_conj
 (*#* ** Properties of the real axis *)
 
 (* UNEXPORTED
-Section cc_IR_properties.
+Section cc_IR_properties
 *)
 
 inline "cic:/CoRN/complex/CComplex/Re_cc_IR.con".
@@ -345,7 +353,7 @@ inline "cic:/CoRN/complex/CComplex/cc_IR_nring.con".
 inline "cic:/CoRN/complex/CComplex/cc_IR_nexp.con".
 
 (* UNEXPORTED
-End cc_IR_properties.
+End cc_IR_properties
 *)
 
 (* UNEXPORTED