%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/CRing_axioms/R.var" "CRing_axioms__".
+alias id "R" = "cic:/CoRN/algebra/CRings/CRing_axioms/R.var".
inline "cic:/CoRN/algebra/CRings/CRing_is_CRing.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/Ring_constructions/R.var" "Ring_constructions__".
+alias id "R" = "cic:/CoRN/algebra/CRings/Ring_constructions/R.var".
(*#*
The multiplicative monoid of a ring is defined as follows.
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/Ring_unfolded/R.var" "Ring_unfolded__".
+alias id "R" = "cic:/CoRN/algebra/CRings/Ring_unfolded/R.var".
(* begin hide *)
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/Ring_basics/R.var" "Ring_basics__".
+alias id "R" = "cic:/CoRN/algebra/CRings/Ring_basics/R.var".
inline "cic:/CoRN/algebra/CRings/one_ap_zero.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/exponentiation/R.var" "exponentiation__".
+alias id "R" = "cic:/CoRN/algebra/CRings/exponentiation/R.var".
(* End_SpecReals *)
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/nat_injection/R.var" "nat_injection__".
+alias id "R" = "cic:/CoRN/algebra/CRings/nat_injection/R.var".
(*#*
The injection of Coq natural numbers into a ring is called [nring].
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/int_injection/R.var" "int_injection__".
+alias id "R" = "cic:/CoRN/algebra/CRings/int_injection/R.var".
(*#*
The injection of Coq integers into a ring is called [zring]. Again,
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/Ring_sums/R.var" "Ring_sums__".
+alias id "R" = "cic:/CoRN/algebra/CRings/Ring_sums/R.var".
(*#*
*** Infinite Ring sums
Section Dist_properties
*)
-inline "cic:/CoRN/algebra/CRings/Dist_properties/R.var" "Dist_properties__".
+alias id "R" = "cic:/CoRN/algebra/CRings/Dist_properties/R.var".
inline "cic:/CoRN/algebra/CRings/dist_1b.con".
Section NExp_properties
*)
-inline "cic:/CoRN/algebra/CRings/NExp_properties/R.var" "NExp_properties__".
+alias id "R" = "cic:/CoRN/algebra/CRings/NExp_properties/R.var".
inline "cic:/CoRN/algebra/CRings/nexp_wd.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/CRing_Ops/R.var" "CRing_Ops__".
+alias id "R" = "cic:/CoRN/algebra/CRings/CRing_Ops/R.var".
-inline "cic:/CoRN/algebra/CRings/CRing_Ops/F.var" "CRing_Ops__".
+alias id "F" = "cic:/CoRN/algebra/CRings/CRing_Ops/F.var".
-inline "cic:/CoRN/algebra/CRings/CRing_Ops/G.var" "CRing_Ops__".
+alias id "G" = "cic:/CoRN/algebra/CRings/CRing_Ops/G.var".
(* begin hide *)
Section Part_Function_Nth_Power
*)
-inline "cic:/CoRN/algebra/CRings/CRing_Ops/Part_Function_Nth_Power/n.var" "CRing_Ops__Part_Function_Nth_Power__".
+alias id "n" = "cic:/CoRN/algebra/CRings/CRing_Ops/Part_Function_Nth_Power/n.var".
inline "cic:/CoRN/algebra/CRings/part_function_nth_strext.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/CRing_Ops/R'.var" "CRing_Ops__".
+alias id "R'" = "cic:/CoRN/algebra/CRings/CRing_Ops/R'.var".
inline "cic:/CoRN/algebra/CRings/included_FMult.con".
inline "cic:/CoRN/algebra/CRings/included_FMult''.con".
-inline "cic:/CoRN/algebra/CRings/CRing_Ops/n.var" "CRing_Ops__".
+alias id "n" = "cic:/CoRN/algebra/CRings/CRing_Ops/n.var".
inline "cic:/CoRN/algebra/CRings/included_FNth.con".
Section ScalarMultiplication
*)
-inline "cic:/CoRN/algebra/CRings/ScalarMultiplication/R.var" "ScalarMultiplication__".
+alias id "R" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/R.var".
-inline "cic:/CoRN/algebra/CRings/ScalarMultiplication/F.var" "ScalarMultiplication__".
+alias id "F" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/F.var".
(* begin hide *)
(* end hide *)
-inline "cic:/CoRN/algebra/CRings/ScalarMultiplication/R'.var" "ScalarMultiplication__".
+alias id "R'" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/R'.var".
inline "cic:/CoRN/algebra/CRings/included_FScalMult.con".