aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
2007-10-04Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o...emakarov
2007-10-03Révision de theories/Logic concernant les axiomes de descriptions.herbelin
2007-10-03BigZ now are provedthery
2007-10-02The following now compiles: abstract integers with plus, minus and times, bin...emakarov
2007-10-02Now NMake is provedthery
2007-10-01Added the compilation of theories/Numbers to Makefile.common. The following t...emakarov
2007-10-01Nouvelle mise à jourherbelin
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
2007-09-28Creation of a new token PATTERNIDENT (?ident) for intro patterns, soglondu
2007-09-28Oubli dans Setoid.vnotin
2007-09-27Découpage de Setoid.vnotin
2007-09-27Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0herbelin
2007-09-26 added a lemma to prove inj_pair2 when eq_dec is available.vsiles
2007-09-25An update on theories/Numbers.emakarov
2007-09-21Update on theories/Numbersemakarov
2007-09-21Update on theories/Numbers. Natural numbers are mostly complete,emakarov
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
2007-09-20Changed the definition of Nminus in BinNat.v by removing comparison.emakarov
2007-09-13Update before joining all signatures into one.emakarov
2007-09-07- renaming Qle_shift_recip_r into Qle_shift_inv_r, etcroconnor
2007-08-28Adding a few lemmas for reasoning about inequalities over the roconnor
2007-08-26Add more equality tactics. Upgrade program_simpl for discrimination of conjun...msozeau
2007-08-13An update on axiomatic number classes.emakarov
2007-08-08Fix dependency bugs due to Program modules renamings.msozeau
2007-08-08Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vemakarov
2007-08-08A better Program documentation. Include it in the generated stdlib doc.msozeau
2007-08-07Move Program tactics into a proper theories/ directory as they are general pu...msozeau
2007-07-30mul and sqrtthery
2007-07-25Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n etnotin
2007-07-24proof of compare addedthery
2007-07-24An update on axiomatization of numbers.emakarov
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
2007-07-18J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir aspiwack
2007-07-13An update on axiomatization of number classes.emakarov
2007-07-13Added Qpower_plus' and Zpower_Qpowerroconnor
2007-07-13Small cleanupletouzey
2007-07-13Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans leherbelin
2007-07-13Deletion of some firstorder calls in FSetAVL: letouzey
2007-07-12Proof for subthery
2007-07-12Deletion of an obsolete file (euclidian division done in old syntax with real...letouzey
2007-07-12normalisation (by closure) was not performed under fixpointsbarras
2007-07-12Proof for succ, add, predthery
2007-07-11Added ForAll_Str_nth_tlroconnor
2007-07-10Big reorganization of romega/ReflOmegaCore.v: towards a modular letouzey
2007-07-06Update of theories/Numbers directory.emakarov
2007-07-05Update on numbers.emakarov
2007-07-05Added Qpower_mult theorem.roconnor
2007-07-03Compatibilité des noms longs de Bool déplacés dans Datatypesherbelin
2007-07-02Correction (partielle) du bug #1587notin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 10:08:09 +0000