diff options
| author | emakarov | 2007-10-23 11:09:40 +0000 |
|---|---|---|
| committer | emakarov | 2007-10-23 11:09:40 +0000 |
| commit | 699c507995fb9ede2eb752a01f90cf6d8caad4de (patch) | |
| tree | 69c9239bb8b5e8e2ecc7b10ba921d51f729dabb8 /theories/Numbers/Integer/NatPairs | |
| parent | d672ce42ecd1fd6845f1c9ea178f5d9fd05afb2c (diff) | |
Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natural numbers are isomorphic. Added NatScope and IntScope for abstract developments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/NatPairs')
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 9a012b26cf..38e8e097ad 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -49,14 +49,14 @@ Notation "x >= y" := (Zle y x) (only parsing) : IntScope. Notation Local N := NZ. (* To remember N without having to use a long qualifying name. since NZ will be redefined *) -Notation Local NE := NZE (only parsing). +Notation Local NE := NZeq (only parsing). Notation Local plus_wd := NZplus_wd (only parsing). Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. Module Export NZAxiomsMod <: NZAxiomsSig. Definition NZ : Set := Z. -Definition NZE := Zeq. +Definition NZeq := Zeq. Definition NZ0 := Z0. Definition NZsucc := Zsucc. Definition NZpred := Zpred. |