diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-02 23:26:13 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-02 23:26:13 +0000 |
| commit | f82bfc64fca9fb46136d7aa26c09d64cde0432d2 (patch) | |
| tree | 471a75d813fb70072c384b926f334e27919cf889 /theories/Numbers/Natural/Abstract/NAxioms.v | |
| parent | b37cc1ad85d2d1ac14abcd896f2939e871705f98 (diff) | |
In abstract parts of theories/Numbers, plus/times becomes add/mul,
for increased consistency with bignums parts
(commit part I: content of files)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index a4e8c056f..c31f216a3 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -24,8 +24,8 @@ Notation N0 := NZ0. Notation N1 := (NZsucc NZ0). Notation S := NZsucc. Notation P := NZpred. -Notation plus := NZplus. -Notation times := NZtimes. +Notation add := NZadd. +Notation mul := NZmul. Notation minus := NZminus. Notation lt := NZlt. Notation le := NZle. @@ -35,9 +35,9 @@ Notation "x == y" := (Neq x y) (at level 70) : NatScope. Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope. Notation "0" := NZ0 : NatScope. Notation "1" := (NZsucc NZ0) : NatScope. -Notation "x + y" := (NZplus x y) : NatScope. +Notation "x + y" := (NZadd x y) : NatScope. Notation "x - y" := (NZminus x y) : NatScope. -Notation "x * y" := (NZtimes x y) : NatScope. +Notation "x * y" := (NZmul x y) : NatScope. Notation "x < y" := (NZlt x y) : NatScope. Notation "x <= y" := (NZle x y) : NatScope. Notation "x > y" := (NZlt y x) (only parsing) : NatScope. |