%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields2/Properties_of_leEq/R.var" "Properties_of_leEq__".
+alias id "R" = "cic:/CoRN/algebra/COrdFields2/Properties_of_leEq/R.var".
(* UNEXPORTED
Section addition
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields2/PosP_properties/R.var" "PosP_properties__".
+alias id "R" = "cic:/CoRN/algebra/COrdFields2/PosP_properties/R.var".
(* begin hide *)
Section One_div_succ_properties
*)
-inline "cic:/CoRN/algebra/COrdFields2/One_div_succ_properties/R.var" "One_div_succ_properties__".
+alias id "R" = "cic:/CoRN/algebra/COrdFields2/One_div_succ_properties/R.var".
inline "cic:/CoRN/algebra/COrdFields2/one_div_succ_resp_leEq.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields2/Half_properties/R.var" "Half_properties__".
+alias id "R" = "cic:/CoRN/algebra/COrdFields2/Half_properties/R.var".
inline "cic:/CoRN/algebra/COrdFields2/half_1.con".