aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2002-10-13Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3124 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
Utilisation du parseur de constr pour les productions des règles de syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3123 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3122 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des ↵barras
letins, ce qui conduisait a des comportement peu intuitifs. On priviligiera l'utilisation de la tactique Subst. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-09Preuve du lemme de Rolledesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3109 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-09MAJ pour modification dans Rcompletdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3107 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-09Suppression d'un lemme redondantdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3106 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-09Proof of Heine's theoremdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3105 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3099 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Quelques resultats complementairesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3096 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Affaiblissement des hypotheses dans TAF_gendesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3095 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-04Ajout du lemme derivable_pt_lim_powerdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3089 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-04Preuve de Bolzano-Weierstrassdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3088 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-02*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3068 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-02Fonctions Ln et puissancedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3067 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-26suppression de l'axiome eqDomdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3037 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25preuve d'un axiome restant via Rtopologydesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3036 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25MAJ pour Rtopologydesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3035 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25Proprietes topologiques dans Rdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3034 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25Affaiblissement de l'ordre sur Z on demande x < y et seulementmohring
que y (et pas x) soit plus garnd que c git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3032 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Preuves dans CC deherbelin
dégénérescence des propositions <-> tiers-exclu /\ extensionnalité propositionnelle et dans CCI de extensionnalité propositionnelle -> indiscernabilité des preuves git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2960 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31MAJ pour TAFdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2950 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31Theoreme des accroissements finis generalises et corollairesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2948 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31MAJ pour Exp_propdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2946 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31Proprietes de l'exponentielledesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2945 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29MAJ pour Rtrigo_regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2934 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29Regularite de sin et cosdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2933 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29Continuite des series de fonctions NCdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2932 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-22Quelques ameliorations dans Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2907 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19Nvll preuves R_dist_tri et tech_limitmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2906 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19Regularites de pow et des sommes finies / MAJ Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2904 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19Resultats de regularite de Rabsolu / MAJ de Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2903 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19Quelques ameliorations...desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2902 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18Correction d'un bug dans IsCont_ptdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2899 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18MAJ pour Sqrt_regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2898 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18Preuves de la continuite/derivabilite de sqrt sur R+/R+*desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2897 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2884 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2883 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Rtrigo pour sqrtdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2880 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2879 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16R_sqr ne contient plus de resultats sur sqrt -> R_sqrtdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2878 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Realsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2877 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Rgeomdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2876 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Proprietes (calculatoires) des fonctions trigonometriquesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2875 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Proprietes de la racine carreedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2874 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Definition de la racine carreedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2873 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15Bug de précédenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2869 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Preuve de cos_plusdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2863 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Quelques resultats supplementaires sur les suites convergentesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2862 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Le theoreme central sur les produits de Cauchy finisdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2861 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 17:24:09 +0000