set "baseuri" "cic:/matita/CoRN-Decl/reals/RealLists".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: RealLists.v,v 1.4 2004/04/23 10:01:05 lcf Exp $ *)
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
*)