%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields/COrdField_axioms/F.var" "COrdField_axioms__".
+alias id "F" = "cic:/CoRN/algebra/COrdFields/COrdField_axioms/F.var".
inline "cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields/OrdField_basics/R.var" "OrdField_basics__".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/OrdField_basics/R.var".
inline "cic:/CoRN/algebra/COrdFields/less_imp_ap.con".
(*#* ** Basic properties of [ [<=] ]
*)
-inline "cic:/CoRN/algebra/COrdFields/Basic_Properties_of_leEq/R.var" "Basic_Properties_of_leEq__".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/Basic_Properties_of_leEq/R.var".
inline "cic:/CoRN/algebra/COrdFields/leEq_wdr.con".
e.g.%\% [x[/]TwoNZ].
*)
-inline "cic:/CoRN/algebra/COrdFields/infinity_of_cordfields/R.var" "infinity_of_cordfields__".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/infinity_of_cordfields/R.var".
inline "cic:/CoRN/algebra/COrdFields/pos_one.con".
*** Consequences of infinity
*)
-inline "cic:/CoRN/algebra/COrdFields/consequences_of_infinity/F.var" "consequences_of_infinity__".
+alias id "F" = "cic:/CoRN/algebra/COrdFields/consequences_of_infinity/F.var".
inline "cic:/CoRN/algebra/COrdFields/square_eq.con".
** Properties of [[<]]
*)
-inline "cic:/CoRN/algebra/COrdFields/Properties_of_Ordering/R.var" "Properties_of_Ordering__".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/Properties_of_Ordering/R.var".
(*#*
We do not use a special predicate for positivity,