aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-11-14Bug implicit argumentsherbelin
2003-11-14Automatisation de la traduction de iff_trans; renommage IFherbelin
2003-11-14Backtrack sur Peanoherbelin
2003-11-14Nouveaux lemmes 'canoniques'; compatibiliteherbelin
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...barras
2003-11-13Oubli report Nul/Posherbelin
2003-11-13Requireherbelin
2003-11-13qq petit ajouts à Zdivletouzey
2003-11-12MAJ INZherbelin
2003-11-12Ajout lemme projectionsherbelin
2003-11-12%type au lieu de %Therbelin
2003-11-12Lemmes dans un sens plus naturelherbelin
2003-11-12Restructuration ZArithherbelin
2003-11-12Cosmetiqueherbelin
2003-11-12Noms canoniques pour les variables lieesherbelin
2003-11-12Independance vis a vis noms variables liees; partie sur bool dans Zboolherbelin
2003-11-12Noms/énoncés plus canoniquesherbelin
2003-11-12Independance vis a vis noms variables lieesherbelin
2003-11-12Ajout lemmes; independance vis a vis noms variables liees; restructurationherbelin
2003-11-12Ajout partie sur bool anciennement dans Zmischerbelin
2003-11-12Ajout lemmes; independance vis a vis noms variables lieesherbelin
2003-11-12On sait jamaisherbelin
2003-11-12petits changements de syntaxebarras
2003-11-09Ajout quelques lemmes; noms des variables lieesherbelin
2003-11-07Oubli BinNatherbelin
2003-11-07Oubli d'un Set Implicit Argumentsherbelin
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatifherbelin
2003-11-07Biblio standard sans impredicativiteherbelin
2003-11-06Des oublisherbelin
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
2003-11-05Notationsherbelin
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...herbelin
2003-11-05Preuve de l'incoherence de {A}+{~A} avec Set impredicatifherbelin
2003-11-05Redondancesherbelin
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...herbelin
2003-11-03Exporting ^; utilisation arg scope impliciteherbelin
2003-11-02Cosmetiqueherbelin
2003-11-02Renforcement significatif du resultat principalherbelin
2003-11-02Rien de bien importantherbelin
2003-11-02Commentairesherbelin
2003-11-02Typoherbelin
2003-11-02AC + EXT -> EMherbelin
2003-11-02Relations entre le choix (forme relationnelle) avec restriction ou nonherbelin
2003-11-02Renommage bool en boolP pour eviter la qualificationherbelin
2003-11-02Restauration preference Rge a Rle pour compatibilite...herbelin
2003-11-02Restauration preference Rge a Rle pour compatibilite...; petit nettoyageherbelin
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...herbelin
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...herbelin
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...herbelin
2003-10-29Choix sous sa forme relationnelleherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 06:33:11 +0000