diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-14 14:39:07 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-14 14:39:07 +0000 |
| commit | 67f72c93f5f364591224a86c52727867e02a8f71 (patch) | |
| tree | ecf630daf8346e77e6620233d8f3e6c18a0c9b3c /theories/Reals/Raxioms.v | |
| parent | b239b208eb9a66037b0c629cf7ccb6e4b110636a (diff) | |
option -dump-glob pour coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Raxioms.v')
| -rw-r--r-- | theories/Reals/Raxioms.v | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index f1aa04519..1c7674f4e 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -9,7 +9,7 @@ (*i $Id$ i*) (*********************************************************) -(*s {Axiomatisation of the classical reals} *) +(** Axiomatisation of the classical reals *) (*********************************************************) Require Export ZArith. @@ -17,10 +17,11 @@ Require Export Rsyntax. Require Export TypeSyntax. (*********************************************************) -(* {Field axioms} *) +(* Field axioms *) (*********************************************************) + (*********************************************************) -(*s Addition *) +(** Addition *) (*********************************************************) (**********) @@ -40,7 +41,7 @@ Axiom Rplus_Ol:(r:R)``0+r==r``. Hints Resolve Rplus_Ol : real. (***********************************************************) -(*s Multiplication *) +(** Multiplication *) (***********************************************************) (**********) @@ -64,7 +65,7 @@ Axiom R1_neq_R0:``1<>0``. Hints Resolve R1_neq_R0 : real. (*********************************************************) -(*s Distributivity *) +(** Distributivity *) (*********************************************************) (**********) @@ -72,17 +73,17 @@ Axiom Rmult_Rplus_distr:(r1,r2,r3:R)``r1*(r2+r3)==(r1*r2)+(r1*r3)``. Hints Resolve Rmult_Rplus_distr : real v62. (*********************************************************) -(* Order axioms *) +(** Order axioms *) (*********************************************************) (*********************************************************) -(*s Total Order *) +(** Total Order *) (*********************************************************) (**********) Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1<r2`` r1==r2) ``r1>r2``). (*********************************************************) -(*s Lower *) +(** Lower *) (*********************************************************) (**********) @@ -101,7 +102,7 @@ Axiom Rlt_monotony:(r,r1,r2:R)``0<r``->``r1<r2``->``r*r1<r*r2``. Hints Resolve Rlt_antisym Rlt_compatibility Rlt_monotony : real. (**********************************************************) -(*s Injection from N to R *) +(** Injection from N to R *) (**********************************************************) (**********) @@ -112,7 +113,7 @@ Fixpoint INR [n:nat]:R:=(Cases n of end). (**********************************************************) -(*s Injection from Z to R *) +(** Injection from [Z] to [R] *) (**********************************************************) (**********) @@ -123,14 +124,14 @@ Definition IZR:Z->R:=[z:Z](Cases z of end). (**********************************************************) -(*s R Archimedian *) +(** [R] Archimedian *) (**********************************************************) (**********) Axiom archimed:(r:R)``(IZR (up r)) > r``/\``(IZR (up r))-r <= 1``. (**********************************************************) -(*s R Complete *) +(** [R] Complete *) (**********************************************************) (**********) |