summaryrefslogtreecommitdiff
path: root/theories/Reals/Raxioms.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /theories/Reals/Raxioms.v
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Reals/Raxioms.v')
-rw-r--r--theories/Reals/Raxioms.v24
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 *)
(**********************************************************)
(**********)