changelog to -rc-1

[helm.git] / matita / contribs / CoRN-Decl / algebra / COrdFields.ma

diff --git a/matita/contribs/CoRN-Decl/algebra/COrdFields.ma b/matita/contribs/CoRN-Decl/algebra/COrdFields.ma
index c68ec867d05355db3b563f6091e37bf469dc1783..cb6476676c55a1c0cbd2aaf1f4d37fe88d19f37b 100644 (file)
--- a/matita/contribs/CoRN-Decl/algebra/COrdFields.ma
+++ b/matita/contribs/CoRN-Decl/algebra/COrdFields.ma
@@ -83,7 +83,7 @@ inline "cic:/CoRN/algebra/COrdFields/is_COrdField.ind".
 
 inline "cic:/CoRN/algebra/COrdFields/COrdField.ind".
 
-coercion "cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con 0 (* compounds *).
 
 (*#*
 %\begin{nameconvention}%
@@ -96,12 +96,20 @@ is written as [pos].
 Implicit Arguments cof_less [c].
 *)
 
+(* NOTATION
+Infix "[<]" := cof_less (at level 70, no associativity).
+*)
+
 inline "cic:/CoRN/algebra/COrdFields/greater.con".
 
 (* UNEXPORTED
 Implicit Arguments greater [F].
 *)
 
+(* NOTATION
+Infix "[>]" := greater (at level 70, no associativity).
+*)
+
 (* End_SpecReals *)
 
 (*#*
@@ -121,8 +129,12 @@ In the names of lemmas, [ [<=] ] is written as [leEq] and
 Implicit Arguments leEq [F].
 *)
 
+(* NOTATION
+Infix "[<=]" := leEq (at level 70, no associativity).
+*)
+
 (* UNEXPORTED
-Section COrdField_axioms.
+Section COrdField_axioms
 *)
 
 (*#*
@@ -132,7 +144,7 @@ Let [F] be a field.
 %\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".
 
@@ -157,7 +169,7 @@ inline "cic:/CoRN/algebra/COrdFields/less_wdr.con".
 inline "cic:/CoRN/algebra/COrdFields/less_wdl.con".
 
 (* UNEXPORTED
-End COrdField_axioms.
+End COrdField_axioms
 *)
 
 (* UNEXPORTED
@@ -169,7 +181,7 @@ Declare Right Step less_wdr.
 *)
 
 (* UNEXPORTED
-Section OrdField_basics.
+Section OrdField_basics
 *)
 
 (*#*
@@ -183,7 +195,7 @@ Let in the rest of this section (and all subsections)
 %\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".
 
@@ -206,13 +218,13 @@ inline "cic:/CoRN/algebra/COrdFields/pos_ap_zero.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
 *)
 
 (*#**********************************)
@@ -220,7 +232,7 @@ 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".
 
@@ -251,7 +263,7 @@ inline "cic:/CoRN/algebra/COrdFields/leEq_transitive.con".
 inline "cic:/CoRN/algebra/COrdFields/less_leEq.con".
 
 (* UNEXPORTED
-End Basic_Properties_of_leEq.
+End Basic_Properties_of_leEq
 *)
 
 (* UNEXPORTED
@@ -263,7 +275,7 @@ Declare Right Step leEq_wdr.
 *)
 
 (* UNEXPORTED
-Section infinity_of_cordfields.
+Section infinity_of_cordfields
 *)
 
 (*#*
@@ -276,7 +288,7 @@ and so on. These are elements of [NonZeros], so that we can write
 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".
 
@@ -307,7 +319,7 @@ inline "cic:/CoRN/algebra/COrdFields/nring_fac_ap_zero.con".
 include "tactics/Opaque_algebra.ma".
 
 (* UNEXPORTED
-Section up_to_four.
+Section up_to_four
 *)
 
 (*#*
@@ -349,11 +361,11 @@ inline "cic:/CoRN/algebra/COrdFields/three_ap_zero.con".
 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 *)
@@ -391,11 +403,11 @@ inline "cic:/CoRN/algebra/COrdFields/twentyfour_ap_zero.con".
 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
@@ -406,15 +418,63 @@ Declare Left Step leEq_wdl.
 Declare Right Step leEq_wdr.
 *)
 
+(* NOTATION
+Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
+*)
+
 (* 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".
 
@@ -425,13 +485,13 @@ Ordered fields have characteristic zero.
 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
 *)
 
 (*#**********************************)
@@ -440,7 +500,7 @@ 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,
@@ -451,7 +511,7 @@ Reasons: it is more natural; in ordinary mathematics we also write [Zero [<] x]
 *)
 
 (* UNEXPORTED
-Section addition.
+Section addition
 *)
 
 (*#*
@@ -533,11 +593,11 @@ inline "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus'.con".
 inline "cic:/CoRN/algebra/COrdFields/qltone.con".
 
 (* UNEXPORTED
-End addition.
+End addition
 *)
 
 (* UNEXPORTED
-Section multiplication.
+Section multiplication
 *)
 
 (*#*
@@ -642,11 +702,11 @@ inline "cic:/CoRN/algebra/COrdFields/pos_div_twentyfour.con".
 inline "cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con".
 
 (* UNEXPORTED
-End multiplication.
+End multiplication
 *)
 
 (* UNEXPORTED
-Section misc.
+Section misc
 *)
 
 (*#*
@@ -674,10 +734,10 @@ inline "cic:/CoRN/algebra/COrdFields/positive_Sumx.con".
 inline "cic:/CoRN/algebra/COrdFields/negative_Sumx.con".
 
 (* UNEXPORTED
-End misc.
+End misc
 *)
 
 (* UNEXPORTED
-End Properties_of_Ordering.
+End Properties_of_Ordering
 *)