aboutsummaryrefslogtreecommitdiff
path: root/theories/QArith
AgeCommit message (Expand)Author
2007-11-24small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough...letouzey
2007-11-06small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is letouzey
2007-11-06Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...letouzey
2007-11-01Adding Qround.v (and helper lemmas and hints)roconnor
2007-11-01In agreement with Laurent Thery, start migration of auxiliary results letouzey
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-07-13Added Qpower_plus' and Zpower_Qpowerroconnor
2007-07-13Small cleanupletouzey
2007-07-05Added Qpower_mult theorem.roconnor
2007-07-02Correction (partielle) du bug #1587notin
2007-06-25Updated Qpow_tac to work on a a more realistic set of exponent values.roconnor
2007-06-21Adding: Field instance for Q.roconnor
2006-12-11Changement dans le kernel : bgregoir
2006-10-17Mise en forme des theoriesnotin
2006-09-29args implicites dans Fieldbarras
2006-09-28separation de RealFieldbarras
2006-09-26commit de field + renommagesbarras
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-09-21better scope/require managment (patch by Russel O'Connor)letouzey
2006-06-25nouvel algorithme pour Zgcd (plus rapide) + un Qcompareletouzey
2006-05-31ajout de QArith dans les theories standardsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 16:48:51 +0000