include "reals/CReals1.ma".
(* UNEXPORTED
-Section Lists.
+Section Lists
*)
(*#* * Lists of Real Numbers
(* begin hide *)
-inline "cic:/CoRN/reals/RealLists/maxlist_aux.con".
+inline "cic:/CoRN/reals/RealLists/Lists/maxlist_aux.con" "Lists__".
(* end hide *)
(* begin hide *)
-inline "cic:/CoRN/reals/RealLists/minlist_aux.con".
+inline "cic:/CoRN/reals/RealLists/Lists/minlist_aux.con" "Lists__".
(* end hide *)
inline "cic:/CoRN/reals/RealLists/leEq_minlist.con".
(* UNEXPORTED
-End Lists.
+End Lists
*)