*)
(* UNEXPORTED
-Section COrdField_axioms.
+Section COrdField_axioms
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/COrdFields/COrdField_axioms/F.var".
inline "cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con".
inline "cic:/CoRN/algebra/COrdFields/less_wdl.con".
(* UNEXPORTED
-End COrdField_axioms.
+End COrdField_axioms
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section OrdField_basics.
+Section OrdField_basics
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/OrdField_basics/R.var".
inline "cic:/CoRN/algebra/COrdFields/less_imp_ap.con".
inline "cic:/CoRN/algebra/COrdFields/leEq_not_eq.con".
(* UNEXPORTED
-End OrdField_basics.
+End OrdField_basics
*)
(*#**********************************)
(* UNEXPORTED
-Section Basic_Properties_of_leEq.
+Section Basic_Properties_of_leEq
*)
(*#**********************************)
(*#* ** Basic properties of [ [<=] ]
*)
-inline "cic:/CoRN/algebra/COrdFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/Basic_Properties_of_leEq/R.var".
inline "cic:/CoRN/algebra/COrdFields/leEq_wdr.con".
inline "cic:/CoRN/algebra/COrdFields/less_leEq.con".
(* UNEXPORTED
-End Basic_Properties_of_leEq.
+End Basic_Properties_of_leEq
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section infinity_of_cordfields.
+Section infinity_of_cordfields
*)
(*#*
e.g.%\% [x[/]TwoNZ].
*)
-inline "cic:/CoRN/algebra/COrdFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/infinity_of_cordfields/R.var".
inline "cic:/CoRN/algebra/COrdFields/pos_one.con".
include "tactics/Opaque_algebra.ma".
(* UNEXPORTED
-Section up_to_four.
+Section up_to_four
*)
(*#*
inline "cic:/CoRN/algebra/COrdFields/four_ap_zero.con".
(* UNEXPORTED
-End up_to_four.
+End up_to_four
*)
(* UNEXPORTED
-Section More_than_four.
+Section More_than_four
*)
(*#* *** Properties of some other numbers *)
inline "cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con".
(* UNEXPORTED
-End More_than_four.
+End More_than_four
*)
(* UNEXPORTED
-End infinity_of_cordfields.
+End infinity_of_cordfields
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section consequences_of_infinity.
+Section consequences_of_infinity
*)
(*#*
*** Consequences of infinity
*)
-inline "cic:/CoRN/algebra/COrdFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/COrdFields/consequences_of_infinity/F.var".
inline "cic:/CoRN/algebra/COrdFields/square_eq.con".
inline "cic:/CoRN/algebra/COrdFields/char0_OrdField.con".
(* UNEXPORTED
-End consequences_of_infinity.
+End consequences_of_infinity
*)
(*#**********************************)
(* UNEXPORTED
-Section Properties_of_Ordering.
+Section Properties_of_Ordering
*)
(*#**********************************)
** Properties of [[<]]
*)
-inline "cic:/CoRN/algebra/COrdFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/Properties_of_Ordering/R.var".
(*#*
We do not use a special predicate for positivity,
*)
(* UNEXPORTED
-Section addition.
+Section addition
*)
(*#*
inline "cic:/CoRN/algebra/COrdFields/qltone.con".
(* UNEXPORTED
-End addition.
+End addition
*)
(* UNEXPORTED
-Section multiplication.
+Section multiplication
*)
(*#*
inline "cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con".
(* UNEXPORTED
-End multiplication.
+End multiplication
*)
(* UNEXPORTED
-Section misc.
+Section misc
*)
(*#*
inline "cic:/CoRN/algebra/COrdFields/negative_Sumx.con".
(* UNEXPORTED
-End misc.
+End misc
*)
(* UNEXPORTED
-End Properties_of_Ordering.
+End Properties_of_Ordering
*)