include "reals/CauchySeq.ma".
(* UNEXPORTED
-Section Maximum.
+Section Maximum
*)
(* UNEXPORTED
-Section Max_function.
+Section Max_function
*)
(*#* ** Maximum, Minimum and Absolute Value
%\end{convention}%
*)
-inline "cic:/CoRN/reals/Max_AbsIR/x.var".
+alias id "x" = "cic:/CoRN/reals/Max_AbsIR/Maximum/Max_function/x.var".
-inline "cic:/CoRN/reals/Max_AbsIR/y.var".
+alias id "y" = "cic:/CoRN/reals/Max_AbsIR/Maximum/Max_function/y.var".
inline "cic:/CoRN/reals/Max_AbsIR/Max_seq.con".
inline "cic:/CoRN/reals/Max_AbsIR/less_MAX_imp.con".
(* UNEXPORTED
-End Max_function.
+End Max_function
*)
inline "cic:/CoRN/reals/Max_AbsIR/MAX_strext.con".
inline "cic:/CoRN/reals/Max_AbsIR/MAX_wd.con".
(* UNEXPORTED
-Section properties_of_Max.
+Section properties_of_Max
*)
(*#* *** Maximum *)
inline "cic:/CoRN/reals/Max_AbsIR/x_div_Max_leEq_x.con".
(* UNEXPORTED
-End properties_of_Max.
+End properties_of_Max
*)
(* UNEXPORTED
-End Maximum.
+End Maximum
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Minimum.
+Section Minimum
*)
(*#* *** Mininum
inline "cic:/CoRN/reals/Max_AbsIR/leEq_Min_plus_eps.con".
-inline "cic:/CoRN/reals/Max_AbsIR/a.var".
+alias id "a" = "cic:/CoRN/reals/Max_AbsIR/Minimum/a.var".
-inline "cic:/CoRN/reals/Max_AbsIR/b.var".
+alias id "b" = "cic:/CoRN/reals/Max_AbsIR/Minimum/b.var".
inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max.con".
inline "cic:/CoRN/reals/Max_AbsIR/Min_less_Max_imp_ap.con".
(* UNEXPORTED
-End Minimum.
+End Minimum
*)
(*#**********************************)
(* UNEXPORTED
-Section Absolute.
+Section Absolute
*)
(*#**********************************)
inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_bnd.con".
(* UNEXPORTED
-End Absolute.
+End Absolute
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Part_Function_Max.
+Section Part_Function_Max
*)
(*#* *** Functional Operators
%\end{convention}%
*)
-inline "cic:/CoRN/reals/Max_AbsIR/F.var".
+alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/F.var".
-inline "cic:/CoRN/reals/Max_AbsIR/G.var".
+alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/G.var".
(* begin hide *)
-inline "cic:/CoRN/reals/Max_AbsIR/P.con".
+inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/P.con" "Part_Function_Max__".
-inline "cic:/CoRN/reals/Max_AbsIR/Q.con".
+inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/Q.con" "Part_Function_Max__".
(* end hide *)
inline "cic:/CoRN/reals/Max_AbsIR/FMax.con".
(* UNEXPORTED
-End Part_Function_Max.
+End Part_Function_Max
*)
(* UNEXPORTED
-Section Part_Function_Abs.
+Section Part_Function_Abs
*)
-inline "cic:/CoRN/reals/Max_AbsIR/F.var".
+alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/F.var".
-inline "cic:/CoRN/reals/Max_AbsIR/G.var".
+alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/G.var".
(* begin hide *)
-inline "cic:/CoRN/reals/Max_AbsIR/P.con".
+inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/P.con" "Part_Function_Abs__".
-inline "cic:/CoRN/reals/Max_AbsIR/Q.con".
+inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/Q.con" "Part_Function_Abs__".
(* end hide *)
inline "cic:/CoRN/reals/Max_AbsIR/FAbs_char.con".
(* UNEXPORTED
-End Part_Function_Abs.
+End Part_Function_Abs
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Inclusion.
+Section Inclusion
*)
-inline "cic:/CoRN/reals/Max_AbsIR/F.var".
+alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/F.var".
-inline "cic:/CoRN/reals/Max_AbsIR/G.var".
+alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/G.var".
(* begin hide *)
-inline "cic:/CoRN/reals/Max_AbsIR/P.con".
+inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/P.con" "Inclusion__".
-inline "cic:/CoRN/reals/Max_AbsIR/Q.con".
+inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/Q.con" "Inclusion__".
(* end hide *)
%\end{convention}%
*)
-inline "cic:/CoRN/reals/Max_AbsIR/R.var".
+alias id "R" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/R.var".
inline "cic:/CoRN/reals/Max_AbsIR/included_FMax.con".
inline "cic:/CoRN/reals/Max_AbsIR/included_FAbs'.con".
(* UNEXPORTED
-End Inclusion.
+End Inclusion
*)
(* UNEXPORTED