aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* *** empty log message ***Gravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2884 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2883 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ Rtrigo pour sqrtGravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2880 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2879 85f007b7-540e-0410-9357-904b9bb8a0f7
* R_sqr ne contient plus de resultats sur sqrt -> R_sqrtGravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2878 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ RealsGravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2877 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ RgeomGravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proprietes (calculatoires) des fonctions trigonometriquesGravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proprietes de la racine carreeGravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Definition de la racine carreeGravatar desmettr2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug de précédenceGravatar herbelin2002-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Preuve de cos_plusGravatar desmettr2002-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques resultats supplementaires sur les suites convergentesGravatar desmettr2002-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le theoreme central sur les produits de Cauchy finisGravatar desmettr2002-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2861 85f007b7-540e-0410-9357-904b9bb8a0f7
* Differents resultats sur les produits finisGravatar desmettr2002-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2860 85f007b7-540e-0410-9357-904b9bb8a0f7
* cos_plus prouveGravatar desmettr2002-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2858 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack pour parser '{x:T|P}*B' sans parenthesesGravatar herbelin2002-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2857 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making the sumbool functions transparent, so that they can used toGravatar bertot2002-07-09
| | | | | | | compute even inside Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2846 85f007b7-540e-0410-9357-904b9bb8a0f7
* certains lemmes sont maintenant dans RtrigoGravatar desmettr2002-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2844 85f007b7-540e-0410-9357-904b9bb8a0f7
* sin_plus prouve (a partir de cos_plus)Gravatar desmettr2002-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2843 85f007b7-540e-0410-9357-904b9bb8a0f7
* sin_bound et cos_bound deplaces dans Rtrigo_altGravatar desmettr2002-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2842 85f007b7-540e-0410-9357-904b9bb8a0f7
* sin_bound et cos_bound sont prouves (merci les series alternees...)Gravatar desmettr2002-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2841 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2002-07-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2836 85f007b7-540e-0410-9357-904b9bb8a0f7
* sin_eq_0 est maintenant prouveGravatar desmettr2002-07-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2835 85f007b7-540e-0410-9357-904b9bb8a0f7
* sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq)Gravatar desmettr2002-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2830 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'axiome arc_sin_cosGravatar desmettr2002-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de IAF, introduction de TAF et preuves de 3 axiomesGravatar desmettr2002-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2822 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2002-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Constructions des séries alternées et de PIGravatar desmettr2002-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2819 85f007b7-540e-0410-9357-904b9bb8a0f7
* PI n'est plus un axiomeGravatar desmettr2002-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Version plus propre de RsigmaGravatar desmettr2002-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de BinomeGravatar desmettr2002-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2814 85f007b7-540e-0410-9357-904b9bb8a0f7
* Formule du binome (pour cos(x+y), sin(x+y)...)Gravatar desmettr2002-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification sin_approxGravatar desmettr2002-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Resolution de bug (du a Auto; remplacement par lt_O_Sn)Gravatar mayero2002-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration de Rcomplet et Alembert_complGravatar desmettr2002-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration de Rcomplet et Alembert_complGravatar desmettr2002-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2805 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'axiome d'extensionnaliteGravatar desmettr2002-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementGravatar filliatr2002-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle version avec INR + Amelioration de Sup0.Gravatar mayero2002-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2801 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2002-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2800 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith_base, Zbool, Bool_natGravatar filliatr2002-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement contrib/correctness/ProgWf -> theories/ZArith/ZwfGravatar filliatr2002-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de fct_eqGravatar desmettr2002-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de exp, cosh et sinhGravatar desmettr2002-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2791 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications relatives a l'ajout de Rtrigo_defGravatar desmettr2002-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Definitions de exp, cos et sinGravatar desmettr2002-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2789 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2002-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2776 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ranalysis.vGravatar desmettr2002-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding file theories/ZArith/Zsqrt.v that contains a square root function.Gravatar bertot2002-06-07
| | | | | | | | | | | | | actually three functions are provided, one working on positive numbers (it is structurally recursive), one with a strong specification (Zsqrt), and one with a weak specification (Zsqrt_plain). For the function with a weak specification an extra theorem is also provided. The decision functions in ZArith_dec have been made transparent so that computation with the square root function also becomes possible with Lazy Beta Iota Delta Zeta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2770 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 11:54:35 +0000