aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2002-07-18Correction d'un bug dans IsCont_ptdesmettr
2002-07-18MAJ pour Sqrt_regdesmettr
2002-07-18Preuves de la continuite/derivabilite de sqrt sur R+/R+*desmettr
2002-07-16*** empty log message ***desmettr
2002-07-16*** empty log message ***desmettr
2002-07-16MAJ Rtrigo pour sqrtdesmettr
2002-07-16*** empty log message ***desmettr
2002-07-16R_sqr ne contient plus de resultats sur sqrt -> R_sqrtdesmettr
2002-07-16MAJ Realsdesmettr
2002-07-16MAJ Rgeomdesmettr
2002-07-16Proprietes (calculatoires) des fonctions trigonometriquesdesmettr
2002-07-16Proprietes de la racine carreedesmettr
2002-07-16Definition de la racine carreedesmettr
2002-07-15Bug de précédenceherbelin
2002-07-12Preuve de cos_plusdesmettr
2002-07-12Quelques resultats supplementaires sur les suites convergentesdesmettr
2002-07-12Le theoreme central sur les produits de Cauchy finisdesmettr
2002-07-12Differents resultats sur les produits finisdesmettr
2002-07-12cos_plus prouvedesmettr
2002-07-11Hack pour parser '{x:T|P}*B' sans parenthesesherbelin
2002-07-09Making the sumbool functions transparent, so that they can used tobertot
2002-07-05certains lemmes sont maintenant dans Rtrigodesmettr
2002-07-05sin_plus prouve (a partir de cos_plus)desmettr
2002-07-05sin_bound et cos_bound deplaces dans Rtrigo_altdesmettr
2002-07-05sin_bound et cos_bound sont prouves (merci les series alternees...)desmettr
2002-07-03*** empty log message ***desmettr
2002-07-03sin_eq_0 est maintenant prouvedesmettr
2002-07-02sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq)desmettr
2002-07-02Suppression de l'axiome arc_sin_cosdesmettr
2002-07-02Modification de IAF, introduction de TAF et preuves de 3 axiomesdesmettr
2002-07-02*** empty log message ***desmettr
2002-07-01Constructions des séries alternées et de PIdesmettr
2002-07-01PI n'est plus un axiomedesmettr
2002-07-01Version plus propre de Rsigmadesmettr
2002-07-01Ajout de Binomedesmettr
2002-07-01Formule du binome (pour cos(x+y), sin(x+y)...)desmettr
2002-07-01Modification sin_approxdesmettr
2002-06-26Resolution de bug (du a Auto; remplacement par lt_O_Sn)mayero
2002-06-25Integration de Rcomplet et Alembert_compldesmettr
2002-06-25Integration de Rcomplet et Alembert_compldesmettr
2002-06-21Suppression de l'axiome d'extensionnalitedesmettr
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
2002-06-20Nouvelle version avec INR + Amelioration de Sup0.mayero
2002-06-20*** empty log message ***desmettr
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-19deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwffilliatr
2002-06-17Suppression de fct_eqdesmettr
2002-06-17Prise en compte de exp, cosh et sinhdesmettr
2002-06-17Modifications relatives a l'ajout de Rtrigo_defdesmettr
2002-06-17Definitions de exp, cos et sindesmettr