- transcript: patched to generate CoRN_notation.ma instead of CoRN.ma

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

diff --git a/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma b/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma
index 48688c5ee681a5bef147b38c0fc7c4178cfa3b41..ff7b399568aef88454acacdee42f85eba0dce44b 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/complex/NRootCC".
 
+include "CoRN_notation.ma".
+
 (* $Id: NRootCC.v,v 1.9 2004/04/23 10:00:55 lcf Exp $ *)
 
 (*#* printing sqrt_Half %\ensuremath{\sqrt{\frac12}}% *)
@@ -26,17 +28,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/complex/NRootCC".
 
 (*#* printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)
 
-(* INCLUDE
-CComplex
-*)
-
-(* INCLUDE
-Wf_nat
-*)
-
-(* INCLUDE
-ArithRing
-*)
+include "complex/CComplex.ma".
 
 (*#* * Roots of Complex Numbers
 
@@ -47,9 +39,9 @@ Properties of non-zero complex numbers
 Section CC_ap_zero.
 *)
 
-inline cic:/CoRN/complex/NRootCC/cc_ap_zero.con.
+inline "cic:/CoRN/complex/NRootCC/cc_ap_zero.con".
 
-inline cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con.
+inline "cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con".
 
 (* UNEXPORTED
 End CC_ap_zero.
@@ -61,7 +53,7 @@ End CC_ap_zero.
 Section Imag_to_Real.
 *)
 
-inline cic:/CoRN/complex/NRootCC/imag_to_real.con.
+inline "cic:/CoRN/complex/NRootCC/imag_to_real.con".
 
 (* UNEXPORTED
 End Imag_to_Real.
@@ -73,25 +65,25 @@ End Imag_to_Real.
 Section NRootI.
 *)
 
-inline cic:/CoRN/complex/NRootCC/sqrt_Half.con.
+inline "cic:/CoRN/complex/NRootCC/sqrt_Half.con".
 
-inline cic:/CoRN/complex/NRootCC/sqrt_I.con.
+inline "cic:/CoRN/complex/NRootCC/sqrt_I.con".
 
-inline cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con.
+inline "cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con".
 
-inline cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con.
+inline "cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con".
 
-inline cic:/CoRN/complex/NRootCC/nroot_I.con.
+inline "cic:/CoRN/complex/NRootCC/nroot_I.con".
 
-inline cic:/CoRN/complex/NRootCC/nroot_I_nexp.con.
+inline "cic:/CoRN/complex/NRootCC/nroot_I_nexp.con".
 
 (* UNEXPORTED
 Hint Resolve nroot_I_nexp: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nroot_minus_I.con.
+inline "cic:/CoRN/complex/NRootCC/nroot_minus_I.con".
 
-inline cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con.
+inline "cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con".
 
 (* UNEXPORTED
 End NRootI.
@@ -117,77 +109,77 @@ Define [c2 := a[^]2[+]b[^]2], [c := sqrt c2], [a'2 := (c[+]a) [*]Half],
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/a.var.
+inline "cic:/CoRN/complex/NRootCC/a.var".
 
-inline cic:/CoRN/complex/NRootCC/b.var.
+inline "cic:/CoRN/complex/NRootCC/b.var".
 
-inline cic:/CoRN/complex/NRootCC/b_.var.
+inline "cic:/CoRN/complex/NRootCC/b_.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/complex/NRootCC/c2.con.
+inline "cic:/CoRN/complex/NRootCC/c2.con".
 
 (* end hide *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con".
 
 (* begin hide *)
 
-inline cic:/CoRN/complex/NRootCC/c.con.
+inline "cic:/CoRN/complex/NRootCC/c.con".
 
-inline cic:/CoRN/complex/NRootCC/a'2.con.
+inline "cic:/CoRN/complex/NRootCC/a'2.con".
 
 (* end hide *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con".
 
 (* begin hide *)
 
-inline cic:/CoRN/complex/NRootCC/a'.con.
+inline "cic:/CoRN/complex/NRootCC/a'.con".
 
-inline cic:/CoRN/complex/NRootCC/b'2.con.
+inline "cic:/CoRN/complex/NRootCC/b'2.con".
 
 (* end hide *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con".
 
 (* begin hide *)
 
-inline cic:/CoRN/complex/NRootCC/b'.con.
+inline "cic:/CoRN/complex/NRootCC/b'.con".
 
 (* end hide *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_a3.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_a3.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_a4.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_a4.con".
 
 (* UNEXPORTED
 Hint Resolve nrCC1_a4: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_a5.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_a5.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_a6.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_a6.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_a6'.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_a6'.con".
 
 (* UNEXPORTED
 Hint Resolve nrCC1_a5: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con".
 
 (* UNEXPORTED
 Hint Resolve nrCC1_a3 nrCC1_a7_upper nrCC1_a7_lower: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con".
 
 (* UNEXPORTED
 End NRootCC_1_ap_real.
@@ -206,19 +198,19 @@ Section NRootCC_1_ap_imag.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/a.var.
+inline "cic:/CoRN/complex/NRootCC/a.var".
 
-inline cic:/CoRN/complex/NRootCC/b.var.
+inline "cic:/CoRN/complex/NRootCC/b.var".
 
-inline cic:/CoRN/complex/NRootCC/a_.var.
+inline "cic:/CoRN/complex/NRootCC/a_.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/complex/NRootCC/c'.con.
+inline "cic:/CoRN/complex/NRootCC/c'.con".
 
-inline cic:/CoRN/complex/NRootCC/a'.con.
+inline "cic:/CoRN/complex/NRootCC/a'.con".
 
-inline cic:/CoRN/complex/NRootCC/b'.con.
+inline "cic:/CoRN/complex/NRootCC/b'.con".
 
 (* end hide *)
 
@@ -226,7 +218,7 @@ inline cic:/CoRN/complex/NRootCC/b'.con.
 Hint Resolve sqrt_I_nexp: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con".
 
 (* UNEXPORTED
 End NRootCC_1_ap_imag.
@@ -234,7 +226,7 @@ End NRootCC_1_ap_imag.
 
 (*#* We now define the roots of arbitrary non zero complex numbers. *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_1.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_1.con".
 
 (* UNEXPORTED
 End NRootCC_1.
@@ -249,17 +241,17 @@ Section NRootCC_2.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/n.var.
+inline "cic:/CoRN/complex/NRootCC/n.var".
 
-inline cic:/CoRN/complex/NRootCC/c.var.
+inline "cic:/CoRN/complex/NRootCC/c.var".
 
-inline cic:/CoRN/complex/NRootCC/z.var.
+inline "cic:/CoRN/complex/NRootCC/z.var".
 
-inline cic:/CoRN/complex/NRootCC/c_.var.
+inline "cic:/CoRN/complex/NRootCC/c_.var".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_2'.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_2'.con".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_2.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_2.con".
 
 (* UNEXPORTED
 End NRootCC_2.
@@ -269,44 +261,44 @@ End NRootCC_2.
 Section NRootCC_3.
 *)
 
-inline cic:/CoRN/complex/NRootCC/Im_poly.con.
+inline "cic:/CoRN/complex/NRootCC/Im_poly.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a1.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a1.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a2.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a2.con".
 
 (*#*
 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)] and [n : nat].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/a.var.
+inline "cic:/CoRN/complex/NRootCC/a.var".
 
-inline cic:/CoRN/complex/NRootCC/b.var.
+inline "cic:/CoRN/complex/NRootCC/b.var".
 
-inline cic:/CoRN/complex/NRootCC/b_.var.
+inline "cic:/CoRN/complex/NRootCC/b_.var".
 
-inline cic:/CoRN/complex/NRootCC/n.var.
+inline "cic:/CoRN/complex/NRootCC/n.var".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_poly''.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_poly''.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a3.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a3.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a4.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a4.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a5.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a5.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a6.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a6.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_poly'.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_poly'.con".
 
 (* UNEXPORTED
 Hint Resolve nrCC3_a3: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a7.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a7.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a8.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a8.con".
 
 (* UNEXPORTED
 Hint Resolve nth_coeff_p_mult_c_: algebra.
@@ -316,15 +308,15 @@ Hint Resolve nth_coeff_p_mult_c_: algebra.
 Hint Resolve nrCC3_a6: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC3_a9.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC3_a9.con".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con".
 
 (* UNEXPORTED
 Hint Resolve nrCC3_a1 nrCC3_a7: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_3_.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_3_.con".
 
 (* UNEXPORTED
 Hint Resolve nrootCC_3_: algebra.
@@ -334,7 +326,7 @@ Hint Resolve nrootCC_3_: algebra.
 Hint Resolve calculate_Im: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_3.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_3.con".
 
 (* UNEXPORTED
 Hint Resolve nrCC3_a2: algebra.
@@ -344,7 +336,7 @@ Hint Resolve nrCC3_a2: algebra.
 Hint Resolve nrCC3_a9: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con".
 
 (* UNEXPORTED
 End NRootCC_3.
@@ -359,17 +351,17 @@ Section NRootCC_3'.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/c.var.
+inline "cic:/CoRN/complex/NRootCC/c.var".
 
-inline cic:/CoRN/complex/NRootCC/n.var.
+inline "cic:/CoRN/complex/NRootCC/n.var".
 
-inline cic:/CoRN/complex/NRootCC/n_.var.
+inline "cic:/CoRN/complex/NRootCC/n_.var".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_3'.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_3'.con".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con".
 
 (* UNEXPORTED
 End NRootCC_3'.
@@ -389,19 +381,19 @@ Section NRootCC_4_ap_real.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/a.var.
+inline "cic:/CoRN/complex/NRootCC/a.var".
 
-inline cic:/CoRN/complex/NRootCC/b.var.
+inline "cic:/CoRN/complex/NRootCC/b.var".
 
-inline cic:/CoRN/complex/NRootCC/b_.var.
+inline "cic:/CoRN/complex/NRootCC/b_.var".
 
-inline cic:/CoRN/complex/NRootCC/n.var.
+inline "cic:/CoRN/complex/NRootCC/n.var".
 
-inline cic:/CoRN/complex/NRootCC/n_.var.
+inline "cic:/CoRN/complex/NRootCC/n_.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/complex/NRootCC/c.con.
+inline "cic:/CoRN/complex/NRootCC/c.con".
 
 (* end hide *)
 
@@ -413,24 +405,24 @@ Section NRootCC_4_solutions.
 Hint Resolve nrootCC_3: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a1.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a1.con".
 
 (*#*
 %\begin{convention}% Let [r2',c2 : IR] and [r2'_ : (r2' [#] Zero)].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/r2'.var.
+inline "cic:/CoRN/complex/NRootCC/r2'.var".
 
-inline cic:/CoRN/complex/NRootCC/c2.var.
+inline "cic:/CoRN/complex/NRootCC/c2.var".
 
-inline cic:/CoRN/complex/NRootCC/r2'_.var.
+inline "cic:/CoRN/complex/NRootCC/r2'_.var".
 
 (* UNEXPORTED
 Hint Resolve nrootCC_3': algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a1'.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a1'.con".
 
 (* UNEXPORTED
 End NRootCC_4_solutions.
@@ -447,53 +439,53 @@ and [(y2[*] (r[^] (2) [+]One)) [^]n [=] a[^] (2) [+]b[^] (2)].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/r.var.
+inline "cic:/CoRN/complex/NRootCC/r.var".
 
-inline cic:/CoRN/complex/NRootCC/r_property.var.
+inline "cic:/CoRN/complex/NRootCC/r_property.var".
 
-inline cic:/CoRN/complex/NRootCC/y2.var.
+inline "cic:/CoRN/complex/NRootCC/y2.var".
 
-inline cic:/CoRN/complex/NRootCC/y2_property.var.
+inline "cic:/CoRN/complex/NRootCC/y2_property.var".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a2.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a2.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a3.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a3.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a4.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a4.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_y.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_y.con".
 
-inline cic:/CoRN/complex/NRootCC/y.con.
+inline "cic:/CoRN/complex/NRootCC/y.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_x.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_x.con".
 
-inline cic:/CoRN/complex/NRootCC/x.con.
+inline "cic:/CoRN/complex/NRootCC/x.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a5.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a5.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a6.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a6.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_z.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_z.con".
 
-inline cic:/CoRN/complex/NRootCC/z.con.
+inline "cic:/CoRN/complex/NRootCC/z.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a7.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a7.con".
 
 (* UNEXPORTED
 Hint Resolve nrCC4_a6: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a8.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a8.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a9.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a9.con".
 
 (* UNEXPORTED
 End NRootCC_4_equations.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC4_a10.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC4_a10.con".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con".
 
 (* UNEXPORTED
 End NRootCC_4_ap_real.
@@ -509,39 +501,39 @@ and [(odd n)]; define [c' := (a[+I*]b) [*]II := a'[+I*]b'].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/a.var.
+inline "cic:/CoRN/complex/NRootCC/a.var".
 
-inline cic:/CoRN/complex/NRootCC/b.var.
+inline "cic:/CoRN/complex/NRootCC/b.var".
 
-inline cic:/CoRN/complex/NRootCC/a_.var.
+inline "cic:/CoRN/complex/NRootCC/a_.var".
 
-inline cic:/CoRN/complex/NRootCC/n.var.
+inline "cic:/CoRN/complex/NRootCC/n.var".
 
-inline cic:/CoRN/complex/NRootCC/n_.var.
+inline "cic:/CoRN/complex/NRootCC/n_.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/complex/NRootCC/c'.con.
+inline "cic:/CoRN/complex/NRootCC/c'.con".
 
-inline cic:/CoRN/complex/NRootCC/a'.con.
+inline "cic:/CoRN/complex/NRootCC/a'.con".
 
-inline cic:/CoRN/complex/NRootCC/b'.con.
+inline "cic:/CoRN/complex/NRootCC/b'.con".
 
 (* end hide *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con".
 
 (* UNEXPORTED
 Hint Resolve nroot_minus_I_nexp: algebra.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con".
 
 (* UNEXPORTED
 End NRootCC_4_ap_imag.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_4.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_4.con".
 
 (* UNEXPORTED
 End NRootCC_4.
@@ -553,9 +545,9 @@ End NRootCC_4.
 Section NRootCC_5.
 *)
 
-inline cic:/CoRN/complex/NRootCC/nrCC_5a2.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC_5a2.con".
 
-inline cic:/CoRN/complex/NRootCC/nrCC_5a3.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC_5a3.con".
 
 (* UNEXPORTED
 Hint Resolve nrCC_5a3: algebra.
@@ -566,13 +558,13 @@ Hint Resolve nrCC_5a3: algebra.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/complex/NRootCC/c.var.
+inline "cic:/CoRN/complex/NRootCC/c.var".
 
-inline cic:/CoRN/complex/NRootCC/c_.var.
+inline "cic:/CoRN/complex/NRootCC/c_.var".
 
-inline cic:/CoRN/complex/NRootCC/nrCC_5a4.con.
+inline "cic:/CoRN/complex/NRootCC/nrCC_5a4.con".
 
-inline cic:/CoRN/complex/NRootCC/nrootCC_5.con.
+inline "cic:/CoRN/complex/NRootCC/nrootCC_5.con".
 
 (* UNEXPORTED
 End NRootCC_5.
@@ -580,5 +572,5 @@ End NRootCC_5.
 
 (*#* Final definition *)
 
-inline cic:/CoRN/complex/NRootCC/CnrootCC.con.
+inline "cic:/CoRN/complex/NRootCC/CnrootCC.con".