diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-17 12:53:34 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-17 12:53:34 +0000 |
commit | 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch) | |
tree | 63cdf18cd47260eb90550f62f7b22e2e2e208f6c /theories/Reals/Raxioms.v | |
parent | 744e7f6a319f4d459a3cc2309f575d43041d75aa (diff) |
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Raxioms.v')
-rw-r--r-- | theories/Reals/Raxioms.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index cb9086317..0f5f04fff 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -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 *) (**********************************************************) (**********) |