aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Expand)AuthorAge
* Détection d'un Fold incorrect suite à correction bug #986Gravatar herbelin2005-07-13
* Détection d'un Fold incorrect suite à correction bug #986Gravatar herbelin2005-07-13
* Missing translating a 'O' into a '0' (again)Gravatar herbelin2005-03-29
* compatibility with POWERPCGravatar gregoire2004-11-22
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* ajout decimal_exp pour interpreter les notations decimalesGravatar mohring2004-03-12
* Suppression de Rsyntax en v8Gravatar herbelin2004-01-13
* bugs avec Pose et AssertGravatar barras2004-01-09
* changement de pose en set (pose n'etait pas utilise avec la semantiqueGravatar barras2003-12-24
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* power associe a droiteGravatar marche2003-12-05
* Ratage standardisation Rge_monotony en Rmult_ge_compat_rGravatar herbelin2003-12-01
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Notation locale pour RpowerGravatar herbelin2003-11-29
* Ajout lemmes, simplification preuve de SeqPropGravatar herbelin2003-11-29
* Utilisation du total_order non constructifGravatar herbelin2003-11-29
* Protection contre les renommages; redondancesGravatar herbelin2003-11-28
* Restauration compatibilite 7.4 pour le Hint Unfold RgtGravatar herbelin2003-11-19
* Meilleure solution pour la compatibiliteGravatar herbelin2003-11-15
* MAJ INZGravatar herbelin2003-11-12
* Restauration preference Rge a Rle pour compatibilite...Gravatar herbelin2003-11-02
* Restauration preference Rge a Rle pour compatibilite...; petit nettoyageGravatar herbelin2003-11-02
* Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...Gravatar herbelin2003-10-30
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* R passe dans Set !Gravatar herbelin2003-10-20
* 20 est uniquement associatif a gaucheGravatar herbelin2003-10-17
* lettac -> setGravatar barras2003-10-16
* Pour eviter des regles redondantes en v7Gravatar herbelin2003-10-16
* FTC_P2 maintenant dans RIneqGravatar herbelin2003-10-16
* Ajout de quelques lemmes clesGravatar herbelin2003-10-16
* Affichage = au lieu de == en v7Gravatar herbelin2003-10-15
* Notations pour l'exponentiationGravatar herbelin2003-10-13
* Notation '^'Gravatar herbelin2003-10-10
* Cacher les .v8Gravatar herbelin2003-10-03
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...Gravatar herbelin2003-09-23
* Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...Gravatar herbelin2003-09-21
* Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...Gravatar herbelin2003-09-19
* Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...Gravatar herbelin2003-09-19
* Ajout et MAJ commandes de scopesGravatar herbelin2003-09-12
* Bind et Delimit pour RGravatar herbelin2003-09-12
* Bind et Delimit pour RGravatar herbelin2003-09-12
* INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...Gravatar herbelin2003-06-12
* niveau 49 devient nextGravatar herbelin2003-05-29
* "INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans RealsGravatar herbelin2003-05-24
* BugGravatar herbelin2003-05-21
* Amelioration presentationGravatar herbelin2003-05-14
* Amelioration affichageGravatar herbelin2003-05-14
* Suppression de 'R' dans la notation == entreGravatar herbelin2003-05-14
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-14 08:53:46 +0000