coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.	emakarov	2007-11-08
\| \| \| \|	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 ↵	emakarov	2007-11-07
\| \| \| \| \| \|	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. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An update of theories/Numbers	emakarov	2007-11-03
\| \| \| \|	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 ↵	emakarov	2007-10-23
\| \| \| \| \| \|	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
*	Added the compilation of theories/Numbers to Makefile.common. The following ↵	emakarov	2007-10-01
\| \| \| \| \| \|	things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers. 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,	emakarov	2007-09-21
\| \| \| \| \| \| \|	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
*	Update before joining all signatures into one.	emakarov	2007-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10119 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An update on axiomatic number classes.	emakarov	2007-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10075 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An update on axiomatization of numbers.	emakarov	2007-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An update on axiomatization of number classes.	emakarov	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10002 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the directory theories/Numbers where axiomatizations and ↵	emakarov	2007-06-29
	implementations (unary, binary, etc.) of different number classes (natural, integer, rational, real, complex, etc.) will be stored.Currently there are axiomatized natural numbers with two implementations and axiomatized integers. Modified Makefile accordingly but dod not include the new files in THEORIESVO yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9916 85f007b7-540e-0410-9357-904b9bb8a0f7