| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2007-10-23 | Added Numbers/Natural/Abstract/NIso.v that proves that any two models of ↵ | emakarov | |
| 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 | |||
| 2007-10-04 | Added the proof (in Numbers/Integers/TreeMod) that tree-like representation ↵ | emakarov | |
| of integers due to Gregoire and Théry satisfies the axioms of integers without order. This refers to integers modulo n, i.e., those that fit trees of certain size, not to BigZ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10178 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |