aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith/BinNat.v
Commit message (Expand)AuthorAge
...
* Replaced BinNat with a new version that is based on theories/Numbers/Natural/...Gravatar emakarov2007-11-07
* Added the compilation of theories/Numbers to Makefile.common. The following t...Gravatar emakarov2007-10-01
* Changed the definition of Nminus in BinNat.v by removing comparison.Gravatar emakarov2007-09-20
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
* Added the following theorems to BinPos:Gravatar emakarov2007-03-30
* qq proprietes de plus sur NcompareGravatar letouzey2006-04-29
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
* ouverture du bon scope (positive_scope) derriere le constructeur Npos de NGravatar letouzey2006-04-06
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* ajout Pnat (suite)Gravatar herbelin2003-11-21
* Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...Gravatar herbelin2003-11-21
* Ordre standard pour l'associativiteGravatar herbelin2003-11-14
* Noms/énoncés plus canoniquesGravatar herbelin2003-11-12
* NotationsGravatar herbelin2003-11-05
* Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...Gravatar herbelin2003-11-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 08:23:36 +0000