| Age | Commit message (Expand) | Author |
|---|
| 2002-07-09 | Making the sumbool functions transparent, so that they can used to | bertot |
| 2002-07-05 | certains lemmes sont maintenant dans Rtrigo | desmettr |
| 2002-07-05 | sin_plus prouve (a partir de cos_plus) | desmettr |
| 2002-07-05 | sin_bound et cos_bound deplaces dans Rtrigo_alt | desmettr |
| 2002-07-05 | sin_bound et cos_bound sont prouves (merci les series alternees...) | desmettr |
| 2002-07-03 | *** empty log message *** | desmettr |
| 2002-07-03 | sin_eq_0 est maintenant prouve | desmettr |
| 2002-07-02 | sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq) | desmettr |
| 2002-07-02 | Suppression de l'axiome arc_sin_cos | desmettr |
| 2002-07-02 | Modification de IAF, introduction de TAF et preuves de 3 axiomes | desmettr |
| 2002-07-02 | *** empty log message *** | desmettr |
| 2002-07-01 | Constructions des séries alternées et de PI | desmettr |
| 2002-07-01 | PI n'est plus un axiome | desmettr |
| 2002-07-01 | Version plus propre de Rsigma | desmettr |
| 2002-07-01 | Ajout de Binome | desmettr |
| 2002-07-01 | Formule du binome (pour cos(x+y), sin(x+y)...) | desmettr |
| 2002-07-01 | Modification sin_approx | desmettr |
| 2002-06-26 | Resolution de bug (du a Auto; remplacement par lt_O_Sn) | mayero |
| 2002-06-25 | Integration de Rcomplet et Alembert_compl | desmettr |
| 2002-06-25 | Integration de Rcomplet et Alembert_compl | desmettr |
| 2002-06-21 | Suppression de l'axiome d'extensionnalite | desmettr |
| 2002-06-21 | Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement | filliatr |
| 2002-06-20 | Nouvelle version avec INR + Amelioration de Sup0. | mayero |
| 2002-06-20 | *** empty log message *** | desmettr |
| 2002-06-20 | ZArith_base, Zbool, Bool_nat | filliatr |
| 2002-06-19 | deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf | filliatr |
| 2002-06-17 | Suppression de fct_eq | desmettr |
| 2002-06-17 | Prise en compte de exp, cosh et sinh | desmettr |
| 2002-06-17 | Modifications relatives a l'ajout de Rtrigo_def | desmettr |
| 2002-06-17 | Definitions de exp, cos et sin | desmettr |
| 2002-06-11 | *** empty log message *** | desmettr |
| 2002-06-11 | Ranalysis.v | desmettr |
| 2002-06-07 | Adding file theories/ZArith/Zsqrt.v that contains a square root function. | bertot |
| 2002-06-06 | Correction non reconnaissance des variables de section dans les afficheurs de... | herbelin |
| 2002-06-05 | affaiblissement hyp de Zmult_reg_left | filliatr |
| 2002-05-31 | Ajout d'occurrences de Field (ne pas enlever) | delahaye |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-05-29 | Introduction de syntaxe convivial +,*,<=,<,>= | herbelin |
| 2002-05-29 | Double Induction prend maintenant des noms d'hyppthèses | herbelin |
| 2002-05-29 | Utilisation d'Infix/Distfix autant que possible | herbelin |
| 2002-05-29 | Contournement des My_special_variable | herbelin |
| 2002-05-29 | Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v | herbelin |
| 2002-05-16 | Ajout Peano_dec et Compare_dec | herbelin |
| 2002-05-16 | suppression de inf_decidable dans ZArith_dec (pour SeachPattern) | filliatr |
| 2002-05-14 | petite erreur de syntaxe | barras |
| 2002-05-14 | ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite | barras |
| 2002-05-14 | encore des lemmes sur Zdiv | filliatr |
| 2002-05-14 | nouveaux lemmes dans Zdiv (Claude Marche) | filliatr |
| 2002-05-07 | lemmes plus_O_n et plus_Sn_m (pour Yves) | filliatr |
| 2002-05-07 | lemmes plus_O_n et plus_Sn_m (pour Yves) | filliatr |
