aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* OubliGravatar herbelin2002-11-14
* JMeq now treated as an equality by tactics.Gravatar courant2002-11-14
* nettoyage preuve limit_compGravatar courant2002-11-14
* Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...Gravatar herbelin2002-11-07
* Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourGravatar herbelin2002-10-23
* Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourGravatar herbelin2002-10-23
* Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...Gravatar herbelin2002-10-22
* Mise en transparence des schémas d'induction bien-fondée sur SetGravatar herbelin2002-10-21
* Niveau d'affichage sumor/sumbool incohérent avec le parsingGravatar herbelin2002-10-21
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
* Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsGravatar herbelin2002-10-18
* Bugs dans la factorisation des règles de parsing de "{ ... } * ..."Gravatar herbelin2002-10-17
* Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsGravatar herbelin2002-10-17
* MAJ pour NewtonIntGravatar desmettr2002-10-14
* Integrale de NewtonGravatar desmettr2002-10-14
* La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsGravatar herbelin2002-10-14
* Mise en place d'ensembles de notations symboliques pour nat, Z et RGravatar herbelin2002-10-13
* NettoyageGravatar herbelin2002-10-13
* Déplacement de + et * aux niveaux de précédence 7 et 6Gravatar herbelin2002-10-13
* Déplacement de + et * aux niveaux de précédence 7 et 6Gravatar herbelin2002-10-13
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* Preuve du lemme de RolleGravatar desmettr2002-10-09
* MAJ pour modification dans RcompletGravatar desmettr2002-10-09
* Suppression d'un lemme redondantGravatar desmettr2002-10-09
* Proof of Heine's theoremGravatar desmettr2002-10-09
* *** empty log message ***Gravatar desmettr2002-10-07
* Quelques resultats complementairesGravatar desmettr2002-10-07
* Affaiblissement des hypotheses dans TAF_genGravatar desmettr2002-10-07
* Ajout du lemme derivable_pt_lim_powerGravatar desmettr2002-10-04
* Preuve de Bolzano-WeierstrassGravatar desmettr2002-10-04
* *** empty log message ***Gravatar desmettr2002-10-02
* Fonctions Ln et puissanceGravatar desmettr2002-10-02
* suppression de l'axiome eqDomGravatar desmettr2002-09-26
* preuve d'un axiome restant via RtopologyGravatar desmettr2002-09-25
* MAJ pour RtopologyGravatar desmettr2002-09-25
* Proprietes topologiques dans RGravatar desmettr2002-09-25
* Affaiblissement de l'ordre sur Z on demande x < y et seulementGravatar mohring2002-09-25
* Preuves dans CC deGravatar herbelin2002-08-13
* MAJ pour TAFGravatar desmettr2002-07-31
* Theoreme des accroissements finis generalises et corollairesGravatar desmettr2002-07-31
* MAJ pour Exp_propGravatar desmettr2002-07-31
* Proprietes de l'exponentielleGravatar desmettr2002-07-31
* MAJ pour Rtrigo_regGravatar desmettr2002-07-29
* Regularite de sin et cosGravatar desmettr2002-07-29
* Continuite des series de fonctions NCGravatar desmettr2002-07-29
* Quelques ameliorations dans RegGravatar desmettr2002-07-22
* Nvll preuves R_dist_tri et tech_limitGravatar mayero2002-07-19
* Regularites de pow et des sommes finies / MAJ RegGravatar desmettr2002-07-19
* Resultats de regularite de Rabsolu / MAJ de RegGravatar desmettr2002-07-19