aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith
Commit message (Expand)AuthorAge
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Report de lemmes de Znumtheory dans Zabs ou BinIntGravatar 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
* Pour les .v8Gravatar herbelin2003-11-14
* PresentationGravatar herbelin2003-11-14
* Ordre standard pour l'associativiteGravatar herbelin2003-11-14
* Noms/énoncés plus canoniquesGravatar herbelin2003-11-12
* Independance vis a vis noms variables lieesGravatar herbelin2003-11-12
* NotationsGravatar herbelin2003-11-05
* Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...Gravatar herbelin2003-11-05