diff options
Diffstat (limited to 'theories/Reals/Raxioms.v')
| -rw-r--r-- | theories/Reals/Raxioms.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 61902568..aaea59f4 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Raxioms.v 6338 2004-11-22 09:10:51Z gregoire $ i*) +(*i $Id: Raxioms.v 9245 2006-10-17 12:53:34Z notin $ i*) (*********************************************************) (** Axiomatisation of the classical reals *) @@ -17,11 +17,11 @@ Require Export Rdefinitions. Open Local Scope R_scope. (*********************************************************) -(* Field axioms *) +(** * Field axioms *) (*********************************************************) (*********************************************************) -(** Addition *) +(** ** Addition *) (*********************************************************) (**********) @@ -41,7 +41,7 @@ Axiom Rplus_0_l : forall r:R, 0 + r = r. Hint Resolve Rplus_0_l: real. (***********************************************************) -(** Multiplication *) +(** ** Multiplication *) (***********************************************************) (**********) @@ -65,7 +65,7 @@ Axiom R1_neq_R0 : 1 <> 0. Hint Resolve R1_neq_R0: real. (*********************************************************) -(** Distributivity *) +(** ** Distributivity *) (*********************************************************) (**********) @@ -74,17 +74,17 @@ Axiom Hint Resolve Rmult_plus_distr_l: real v62. (*********************************************************) -(** Order axioms *) +(** * Order axioms *) (*********************************************************) (*********************************************************) -(** Total Order *) +(** ** Total Order *) (*********************************************************) (**********) Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}. (*********************************************************) -(** Lower *) +(** ** Lower *) (*********************************************************) (**********) @@ -103,7 +103,7 @@ Axiom Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. (**********************************************************) -(** Injection from N to R *) +(** * Injection from N to R *) (**********************************************************) (**********) @@ -117,7 +117,7 @@ Arguments Scope INR [nat_scope]. (**********************************************************) -(** Injection from [Z] to [R] *) +(** * Injection from [Z] to [R] *) (**********************************************************) (**********) @@ -130,14 +130,14 @@ Definition IZR (z:Z) : R := Arguments Scope IZR [Z_scope]. (**********************************************************) -(** [R] Archimedian *) +(** * [R] Archimedian *) (**********************************************************) (**********) Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1. (**********************************************************) -(** [R] Complete *) +(** * [R] Complete *) (**********************************************************) (**********) |