coq/theories/Numbers/Integer/Abstract/ZOrder.v, branch master

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

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

An update of theories/Numbers

2007-11-03T19:20:51+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10285 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 transitivity and irreflexivity of <, as well as < -elimination for binary positive numbers.

2007-10-16T16:28:17+00:00

Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 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

Update on theories/Numbers. Natural numbers are mostly complete,

2007-09-21T13:22:41+00:00

need to make NZOrdAxiomsSig a subtype of NAxiomsSig.


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