aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Expand)Author
2005-07-13Détection d'un Fold incorrect suite à correction bug #986herbelin
2005-07-13Détection d'un Fold incorrect suite à correction bug #986herbelin
2005-03-29Missing translating a 'O' into a '0' (again)herbelin
2004-11-22compatibility with POWERPCgregoire
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2004-03-12ajout decimal_exp pour interpreter les notations decimalesmohring
2004-01-13Suppression de Rsyntax en v8herbelin
2004-01-09bugs avec Pose et Assertbarras
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-12-05power associe a droitemarche
2003-12-01Ratage standardisation Rge_monotony en Rmult_ge_compat_rherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-29Notation locale pour Rpowerherbelin
2003-11-29Ajout lemmes, simplification preuve de SeqPropherbelin
2003-11-29Utilisation du total_order non constructifherbelin
2003-11-28Protection contre les renommages; redondancesherbelin
2003-11-19Restauration compatibilite 7.4 pour le Hint Unfold Rgtherbelin
2003-11-15Meilleure solution pour la compatibiliteherbelin
2003-11-12MAJ INZherbelin
2003-11-02Restauration preference Rge a Rle pour compatibilite...herbelin
2003-11-02Restauration preference Rge a Rle pour compatibilite...; petit nettoyageherbelin
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...herbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-20R passe dans Set !herbelin
2003-10-1720 est uniquement associatif a gaucheherbelin
2003-10-16lettac -> setbarras
2003-10-16Pour eviter des regles redondantes en v7herbelin
2003-10-16FTC_P2 maintenant dans RIneqherbelin
2003-10-16Ajout de quelques lemmes clesherbelin
2003-10-15Affichage = au lieu de == en v7herbelin
2003-10-13Notations pour l'exponentiationherbelin
2003-10-10Notation '^'herbelin
2003-10-03Cacher les .v8herbelin
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-19Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...herbelin
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...herbelin
2003-09-12Ajout et MAJ commandes de scopesherbelin
2003-09-12Bind et Delimit pour Rherbelin
2003-09-12Bind et Delimit pour Rherbelin
2003-06-12INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...herbelin
2003-05-29niveau 49 devient nextherbelin
2003-05-24"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Realsherbelin
2003-05-21Bugherbelin
2003-05-14Amelioration presentationherbelin
2003-05-14Amelioration affichageherbelin
2003-05-14Suppression de 'R' dans la notation == entreherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 14:19:16 +0000