index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Reals
Commit message (
Expand
)
Author
Age
*
*** empty log message ***
desmettr
2002-07-16
*
MAJ Rtrigo pour sqrt
desmettr
2002-07-16
*
*** empty log message ***
desmettr
2002-07-16
*
R_sqr ne contient plus de resultats sur sqrt -> R_sqrt
desmettr
2002-07-16
*
MAJ Reals
desmettr
2002-07-16
*
MAJ Rgeom
desmettr
2002-07-16
*
Proprietes (calculatoires) des fonctions trigonometriques
desmettr
2002-07-16
*
Proprietes de la racine carree
desmettr
2002-07-16
*
Definition de la racine carree
desmettr
2002-07-16
*
Preuve de cos_plus
desmettr
2002-07-12
*
Quelques resultats supplementaires sur les suites convergentes
desmettr
2002-07-12
*
Le theoreme central sur les produits de Cauchy finis
desmettr
2002-07-12
*
Differents resultats sur les produits finis
desmettr
2002-07-12
*
cos_plus prouve
desmettr
2002-07-12
*
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-05
*
*** empty log message ***
desmettr
2002-07-03
*
sin_eq_0 est maintenant prouve
desmettr
2002-07-03
*
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-02
*
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-07-01
*
Resolution de bug (du a Auto; remplacement par lt_O_Sn)
mayero
2002-06-26
*
Integration de Rcomplet et Alembert_compl
desmettr
2002-06-25
*
Integration de Rcomplet et Alembert_compl
desmettr
2002-06-25
*
Suppression de l'axiome d'extensionnalite
desmettr
2002-06-21
*
Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement
filliatr
2002-06-21
*
Nouvelle version avec INR + Amelioration de Sup0.
mayero
2002-06-20
*
*** empty log message ***
desmettr
2002-06-20
*
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-17
*
*** empty log message ***
desmettr
2002-06-11
*
Ranalysis.v
desmettr
2002-06-11
*
Correction non reconnaissance des variables de section dans les afficheurs de...
herbelin
2002-06-06
*
Ajout d'occurrences de Field (ne pas enlever)
delahaye
2002-05-31
*
Double Induction prend maintenant des noms d'hyppthèses
herbelin
2002-05-29
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
Optimisation
desmettr
2002-04-02
*
Suppression PI_lb et PI_ub
desmettr
2002-04-02
*
Suppression Field
desmettr
2002-04-02
[next]