Section Interval_definition
*)
-inline "cic:/CoRN/reals/Q_dense/Interval_definition/OF.var" "Interval_definition__".
+alias id "OF" = "cic:/CoRN/reals/Q_dense/Interval_definition/OF.var".
inline "cic:/CoRN/reals/Q_dense/Interval.ind".
Section COrdField_extra
*)
-inline "cic:/CoRN/reals/Q_dense/COrdField_extra/OF.var" "COrdField_extra__".
+alias id "OF" = "cic:/CoRN/reals/Q_dense/COrdField_extra/OF.var".
inline "cic:/CoRN/reals/Q_dense/AbsSmall_pos_reflexive.con".
(*#*** WARNING: A file is being loaded *****)
-inline "cic:/CoRN/reals/Q_dense/Rational_sequence/R1.var" "Rational_sequence__".
+alias id "R1" = "cic:/CoRN/reals/Q_dense/Rational_sequence/R1.var".
inline "cic:/CoRN/reals/Q_dense/start_l.con".