coq - The formal proof system

Age	Commit message (Collapse)	Author
2007-11-16	Added theorems; created NZPlusOrder from NTimesOrder.	emakarov
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10325 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16	Added transitivity and irreflexivity of <, as well as < -elimination for ↵	emakarov
	binary positive numbers. 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
2007-10-01	Added the compilation of theories/Numbers to Makefile.common. The following ↵	emakarov
	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
2007-09-21	Update on theories/Numbers. Natural numbers are mostly complete,	emakarov
	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