aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Expand)Author
2003-10-20R passe dans Set !herbelin
2003-10-1720 est uniquement associatif a gaucheherbelin
2003-10-16lettac -> setbarras
2003-10-16Pour eviter des regles redondantes en v7herbelin
2003-10-16FTC_P2 maintenant dans RIneqherbelin
2003-10-16Ajout de quelques lemmes clesherbelin
2003-10-15Affichage = au lieu de == en v7herbelin
2003-10-13Notations pour l'exponentiationherbelin
2003-10-10Notation '^'herbelin
2003-10-03Cacher les .v8herbelin
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-19Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...herbelin
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...herbelin
2003-09-12Ajout et MAJ commandes de scopesherbelin
2003-09-12Bind et Delimit pour Rherbelin
2003-09-12Bind et Delimit pour Rherbelin
2003-06-12INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...herbelin
2003-05-29niveau 49 devient nextherbelin
2003-05-24"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Realsherbelin
2003-05-21Bugherbelin
2003-05-14Amelioration presentationherbelin
2003-05-14Amelioration affichageherbelin
2003-05-14Suppression de 'R' dans la notation == entreherbelin
2003-05-14Suppression de 'R' dans la notation == entreherbelin
2003-05-14Deplacement lemmes sur fact de Reals vers Arithherbelin
2003-04-29En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...herbelin
2003-04-17Diversherbelin
2003-04-17<> maintenant standardherbelin
2003-04-16suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom differentletouzey
2003-04-16sumboolT, sumorT, sigTT, SigT redondantsherbelin
2003-04-14Local 'o'herbelin
2003-04-12Open Scope en Localherbelin
2003-04-10Remplacement Import par Open Scope en v8herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-04-07Nommage explicite des hypotheses introduites quand le nom existe aussi comme ...herbelin
2003-04-07Espaces superflusherbelin
2003-03-31Ajout Implicit Variable Typeherbelin
2003-03-21*** empty log message ***barras
2003-03-12*** empty log message ***barras
2003-02-27Restructuration des hints pour qu'Auto fasse moins de détours et lesherbelin
2003-02-14Ajout du theoreme de Cesarodesmettr
2003-01-28MAJ pour Regdesmettr
2003-01-22Documentation du contenu de REALSdesmettr
2003-01-22Modifications dans SeqPropdesmettr
2003-01-22Renommages dans Rtrigo_defdesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommages nombreuxdesmettr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 18:47:23 +0000