coq/theories/Numbers/Natural/Abstract/NPlus.v, branch master

In abstract parts of theories/Numbers, plus/times becomes add/mul,

2008-06-03T00:04:16+00:00

for increased consistency with bignums parts 

(commit part II: names of files + additional translation minus --> sub)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7

In abstract parts of theories/Numbers, plus/times becomes add/mul,

2008-06-02T23:26:13+00:00

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

Coq headers + $ in theories/Numbers files

2008-05-15T21:58:20+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7

An update on Numbers. Added two files dealing with recursion, for information only.

2007-11-22T14:34:44+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10330 85f007b7-540e-0410-9357-904b9bb8a0f7

Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder on MacOS.

2007-11-14T19:47:46+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7

Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.

2007-11-08T17:06:32+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10304 85f007b7-540e-0410-9357-904b9bb8a0f7

Replaced BinNat with a new version that is based on theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers.

2007-11-07T18:39:28+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7

Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natural numbers are isomorphic. Added NatScope and IntScope for abstract developments.

2007-10-23T11:09:40+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10247 85f007b7-540e-0410-9357-904b9bb8a0f7

Added the compilation of theories/Numbers to Makefile.common. The following things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers.

2007-10-01T20:21:28+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10161 85f007b7-540e-0410-9357-904b9bb8a0f7

An update on theories/Numbers.

2007-09-25T13:13:41+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10142 85f007b7-540e-0410-9357-904b9bb8a0f7