diff options
| author |  mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-25 20:24:10 +0000 |
|---|---|---|
| committer | mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-25 20:24:10 +0000 |
| commit | e5659553469032c61b076645b98f29f8d4e70d3d (patch) | |
| tree | 8d92d061fef58488c3caa84db4dd1e8a04b45c38 /theories/Reals/Raxioms.v | |
| parent | b2013fcb2c2d6e760610420ff22f0645f7b1f7ad (diff) | |
Modif de l'axiomatisation pour enlever les /\ de _ne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1278 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Raxioms.v')
| -rw-r--r-- | theories/Reals/Raxioms.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index a9c3f621d..38c423938 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -29,8 +29,8 @@ Axiom Rplus_Ropp_r:(r:R)``r+(-r)==0``. Hints Resolve Rplus_Ropp_r : real v62. (**********) -Axiom Rplus_ne:(r:R)``r+0==r``/\``0+r==r``. -Hints Resolve Rplus_ne : real v62. +Axiom Rplus_Ol:(r:R)``0+r==r``. +Hints Resolve Rplus_Ol : real. (***********************************************************) (*s Multiplication *) @@ -48,10 +48,9 @@ Hints Resolve Rmult_assoc : real v62. Axiom Rinv_l:(r:R)``r<>0``->``(1/r)*r==1``. Hints Resolve Rinv_l : real. - (**********) -Axiom Rmult_ne:(r:R)``r*1==r``/\``1*r==r``. -Hints Resolve Rmult_ne : real v62. +Axiom Rmult_1l:(r:R)``1*r==r``. +Hints Resolve Rmult_1l : real. (**********) Axiom R1_neq_R0:``1<>0``. |