(* End_SpecReals *)
(* UNEXPORTED
-Section AbsSmall_properties.
+Section AbsSmall_properties
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdAbs/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdAbs/AbsSmall_properties/R.var".
inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdr.con".
(* begin hide *)
+(* NOTATION
+Notation ZeroR := (Zero:R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_leEq_trans.con".
inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_approach_zero.con".
(* UNEXPORTED
-End AbsSmall_properties.
+End AbsSmall_properties
*)
(* UNEXPORTED
inline "cic:/CoRN/algebra/COrdAbs/absBig.con".
+(* NOTATION
+Notation AbsBig := (absBig _).
+*)
+
inline "cic:/CoRN/algebra/COrdAbs/AbsBigSmall_minus.con".
(* UNEXPORTED
-Section absBig_wd_properties.
+Section absBig_wd_properties
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdAbs/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdAbs/absBig_wd_properties/R.var".
inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr.con".
inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl_unfolded.con".
(* UNEXPORTED
-End absBig_wd_properties.
+End absBig_wd_properties
*)
(* UNEXPORTED