aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2002-11-27Retour sur associativité à droite de * pour compatibilité de prodherbelin
2002-11-26Ne pas cacher les Metas d'une notations, ils peuvent être liant dansherbelin
2002-11-26MAJdesmettr
2002-11-26Theorie 'light' des réelsdesmettr
2002-11-26Explicitation de NONA car sinon LEFTA par défaut; déplacement dans 5herbelin
2002-11-26Plus d'indication pour le gestionnaire de niveauxherbelin
2002-11-26Correction affichage entiers en cas d'échecherbelin
2002-11-26Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesherbelin
2002-11-26Bug niveauherbelin
2002-11-25Rétablissement affichage des entiers de natherbelin
2002-11-25Retablissement SynDef Value/Errorherbelin
2002-11-25Oubliherbelin
2002-11-24Traitement des parenthèses de nat au niveau du printerherbelin
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-11-24Généralisation de l'utilisation de Notationherbelin
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-11-20Les parenthèses de la notation '(n)' maintemant mises par ML pour un meilleu...herbelin
2002-11-18Definition et proprietes de l'integrale de Riemanndesmettr
2002-11-18Proprietes des fonctions en escalierdesmettr
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-14Oubliherbelin
2002-11-14JMeq now treated as an equality by tactics.courant
2002-11-14nettoyage preuve limit_compcourant
2002-11-07Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...herbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-21Mise en transparence des schémas d'induction bien-fondée sur Setherbelin
2002-10-21Niveau d'affichage sumor/sumbool incohérent avec le parsingherbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-18Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsherbelin
2002-10-17Bugs dans la factorisation des règles de parsing de "{ ... } * ..."herbelin
2002-10-17Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsherbelin
2002-10-14MAJ pour NewtonIntdesmettr
2002-10-14Integrale de Newtondesmettr
2002-10-14La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsherbelin
2002-10-13Mise en place d'ensembles de notations symboliques pour nat, Z et Rherbelin
2002-10-13Nettoyageherbelin
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des le...barras
2002-10-09Preuve du lemme de Rolledesmettr
2002-10-09MAJ pour modification dans Rcompletdesmettr
2002-10-09Suppression d'un lemme redondantdesmettr
2002-10-09Proof of Heine's theoremdesmettr
2002-10-07*** empty log message ***desmettr
2002-10-07Quelques resultats complementairesdesmettr
2002-10-07Affaiblissement des hypotheses dans TAF_gendesmettr
2002-10-04Ajout du lemme derivable_pt_lim_powerdesmettr
2002-10-04Preuve de Bolzano-Weierstrassdesmettr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 07:49:39 +0000