aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
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
2002-06-11*** empty log message ***desmettr
2002-06-11Ranalysis.vdesmettr
2002-06-07Adding file theories/ZArith/Zsqrt.v that contains a square root function.bertot
2002-06-06Correction non reconnaissance des variables de section dans les afficheurs de...herbelin
2002-06-05affaiblissement hyp de Zmult_reg_leftfilliatr
2002-05-31Ajout d'occurrences de Field (ne pas enlever)delahaye
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Introduction de syntaxe convivial +,*,<=,<,>=herbelin
2002-05-29Double Induction prend maintenant des noms d'hyppthèsesherbelin
2002-05-29Utilisation d'Infix/Distfix autant que possibleherbelin
2002-05-29Contournement des My_special_variableherbelin
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
2002-05-16Ajout Peano_dec et Compare_decherbelin
2002-05-16suppression de inf_decidable dans ZArith_dec (pour SeachPattern)filliatr
2002-05-14petite erreur de syntaxebarras
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
2002-05-14encore des lemmes sur Zdivfilliatr
2002-05-14nouveaux lemmes dans Zdiv (Claude Marche)filliatr
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
2002-05-06Cosmétiqueherbelin
2002-05-06Standardisationherbelin
2002-04-19lemmes sur Zdiv/Zmodfilliatr
2002-04-19un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...filliatr
2002-04-17*** empty log message ***werner
2002-04-17Quelques bugs avec inject_natherbelin
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-04-08Zdiv -> Export ZArithfilliatr
2002-04-08syntaxe pour Zdiv et Zmodfilliatr
2002-04-05simplification preuvefilliatr
2002-04-05nouveau module Zdivfilliatr
2002-04-02Optimisationdesmettr
2002-04-02Suppression PI_lb et PI_ubdesmettr
2002-04-02Suppression Fielddesmettr
2002-03-29sans utiliser Fielddesmettr
2002-03-29Suppression des invocations a Fielddesmettr
2002-03-26Prise en compte des dependances dans la tactique Casemohring
2002-03-22*** empty log message ***werner
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...herbelin
2002-03-21Intuition ne fait plus de Unfold des constantes (il faut les fairecourant
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-15 06:32:38 +0000