set "baseuri" "cic:/matita/CoRN-Decl/reals/RealFuncts".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: RealFuncts.v,v 1.4 2004/04/07 15:08:10 lcf Exp $ *)
(* end hide *)
(* UNEXPORTED
-Section Continuity.
+Section Continuity
*)
-inline "cic:/CoRN/reals/RealFuncts/f.var".
+alias id "f" = "cic:/CoRN/reals/RealFuncts/Continuity/f.var".
-inline "cic:/CoRN/reals/RealFuncts/f2.var".
+alias id "f2" = "cic:/CoRN/reals/RealFuncts/Continuity/f2.var".
(*#*
Let [f] be a unary setoid operation on [IR] and
*)
(* UNEXPORTED
-End Continuity.
+End Continuity
*)
(* begin hide *)