aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Expand)Author
2003-01-22Commentairesdesmettr
2003-01-22Renommage f_pos -> IVT (Intermediate Value Theoremdesmettr
2003-01-22Suppression d'un Import R_scope probablement oubliedesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommages dans RListdesmettr
2003-01-22MAJ pour renommage Rcompletdesmettr
2003-01-22Renommages dans Rcompletedesmettr
2003-01-22Renommage Rcomplet.v -> Rcomplete.vdesmettr
2003-01-22Suppression de lemmes superflusdesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommages dans PartSumdesmettr
2003-01-21Renommage dans MVTdesmettr
2003-01-21MAJ dans Exp_propdesmettr
2003-01-21Renommage dans Binomial.vdesmettr
2003-01-21Binome.v -> Binomial.vdesmettr
2003-01-21MAJ ArithPropdesmettr
2003-01-21Renommage dans AltSeries.vdesmettr
2003-01-21Renommage dans Alembert.vdesmettr
2003-01-21Quelques améliorationsdesmettr
2003-01-21Suppression de INR2 / Conséquence logique de la nouvelle représentation des...desmettr
2003-01-21Quelques optimisations...desmettr
2003-01-20Cgt définition de platdesmettr
2003-01-20Amélioration de DiscrRdesmettr
2003-01-20Utilisation de 'Recursive' pour les tactiques récursivesherbelin
2003-01-20Utilisation de 'Recursive' pour les tactiques récursivesherbelin
2003-01-19Clear sur hypothese non definieherbelin
2003-01-17Optimisations pour Sup et RComputedesmettr
2003-01-16Ajout de RComputedesmettr
2003-01-16Ajout de la tactique Supdesmettr
2003-01-16renommage de TAF.v en MVT.vdesmettr
2003-01-16Correction d'un petit bug dans Sup0desmettr
2003-01-16Renommage de RealsB en Rbasedesmettr
2003-01-16Renommage de Rbase.v en RIneq.vdesmettr
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
2002-12-15Ajout syntaxe '>'herbelin
2002-12-15Pas d'associativite pour =_Dherbelin
2002-11-27cond_pos -> cond_positivity pour cause de conflit avec posreal...desmettr
2002-11-27Réorganisation de la librairie des réelsdesmettr
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-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...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-14nettoyage preuve limit_compcourant
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-14MAJ pour NewtonIntdesmettr
2002-10-14Integrale de Newtondesmettr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 13:36:58 +0000