]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/library/nat
case not unfilding fixed
[helm.git] / helm / software / matita / library / nat /
2008-05-27 Enrico Tassiauto calls cleanup\
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-04-02 Enrico Tassiremoved dummy rewrite
2008-04-02 Enrico Tassiremoved dummy rewrite
2008-03-26 Wilmer RicciottiReorganization of list library (step 1)
2008-03-25 Wilmer Ricciottismall update
2008-03-12 Claudio Sacerdoti... Problem solved (was: apply needed an argument to avoid...
2008-03-12 Andrea AspertiNuova dimostrazione riflessiva di le_to_Bertrand.
2008-03-10 Claudio Sacerdoti... Scripts fixed because of:
2008-03-06 Enrico Tassi* please let the library in shape *
2008-03-06 Enrico Tassifixed
2008-02-27 Wilmer Ricciottithe proof of bertrand's conjecture is now complete
2008-02-22 Wilmer Ricciottisieve of erathostene (proof of soundness almost done)
2008-02-19 Andrea AspertiAdded o.ma (some results about the magnitude of functio...
2008-02-18 Andrea AspertiComplete proof of Bertrand for n >= 256.
2008-02-14 Andrea AspertiPrima versione di bertrand. Tanti cambiamenti qua e la.
2008-02-08 Andrea Aspertiprogress.
2008-02-07 Andrea AspertiResults about Chebyshev teta function.
2008-02-05 Andrea AspertiSome more theorems.
2008-02-05 Wilmer Ricciottilower bound for neper's constant
2008-02-04 Andrea AspertiImproved approximations for A and prim.
2008-02-04 Andrea AspertiSome improvement.
2008-01-31 Wilmer RicciottiSquare root added.
2008-01-30 Andrea AspertiImproved approximations
2008-01-29 Andrea AspertiNew approximtions.
2008-01-22 Wilmer RicciottiBertrand's conjecture (weak), some work in progress
2008-01-15 Wilmer Ricciottiupdate: upper bound for prim
2008-01-14 Wilmer RicciottiChebyshev's upper bound on prim
2007-12-21 Wilmer Ricciottibeginning proof of chebyshev's bound on prim.
2007-12-17 Wilmer Ricciottiupper bound for logarithmic summation
2007-12-17 Andrea AspertiA few more lemmas.
2007-12-13 Andrea AspertiSome inequalities.
2007-12-12 Wilmer RicciottiProgress.
2007-12-11 Andrea AspertiPartial progress.
2007-12-10 Andrea AspertiMain result for e.
2007-12-10 Andrea AspertiRestructuring.
2007-12-10 Andrea AspertiMain inequalities for e.
2007-12-09 Wilmer RicciottiAdded summation formula for the power of a binomial.
2007-12-07 Andrea AspertiBinomial coefficients and costant e.
2007-12-07 Andrea AspertiA few more theorems.
2007-12-03 Andrea AspertiSome progress.
2007-11-26 Andrea AspertiAlmost there.
2007-11-22 Andrea AspertiBig progress
2007-11-19 Andrea AspertiTowards chebyshev.
2007-10-14 Claudio Sacerdoti... Some lemmas moves to the file they belong to.
2007-10-14 Cristian ArmentanoTheorem sigma_p_knm changed into generic_iter_p_knm.
2007-10-12 Claudio Sacerdoti... Move to OCaml 3.10. Requires debian packages from unsta...
2007-10-12 Andrea AspertiMore restructuring in moebius.ma
2007-10-12 Andrea AspertiReorganization of the library.
2007-09-20 Cristian ArmentanoFurther simplifications to the main theorem about Euler...
2007-09-19 Cristian Armentano* Some simplifications to theorem in file totient1.ma.
2007-09-18 Cristian Armentanosome theorems have been moved to more appropriate files...
2007-09-17 Cristian Armentanotemporary changes, before the complete cancellation...
2007-09-17 Cristian Armentanosimplified version of a theorem.
2007-09-17 Andrea AspertiA new function.
2007-09-11 Cristian Armentanosome theorem names changed.
2007-09-10 Cristian Armentanoother simplifications.
2007-09-09 Cristian Armentanoother simplifications.
2007-09-07 Cristian Armentanosome simplifications.
2007-09-06 Cristian ArmentanoSome simplifications.
2007-08-16 Cristian Armentanolittle change to theorem eq_gcd_times_times_eqv_times_gcd
2007-07-31 Andrea Aspertiremoved generic_sigma_p since generic_iter_p is the...
2007-07-30 Cristian Armentanorenamed generic_sigma_p.ma to generic_iter_p.ma
2007-07-23 Claudio Sacerdoti... Prototype of min_aux changed.
2007-07-06 Enrico Tassimaxipatch for support of multiple DBs.
2007-06-30 Cristian ArmentanoNew definition of Euler's totient function.
2007-06-29 Cristian Armentanogeneric version, specializing generic_sigma_p.ma
2007-06-29 Cristian Armentanotheorems about sigma_p proved using sigma_p_gen
2007-06-27 Cristian Armentanonew gcd properties, and theorems for totient, and theor...
2007-06-26 Cristian Armentano(no commit message)
2007-06-26 Cristian Armentanogeneric sommatory.
2007-05-24 Enrico Tassiauto and autogui... some work
2007-05-17 Enrico Tassiauto rewritten with only one tail recursive function.
2007-05-09 Andrea AspertiA few extensions for the moebius inversion theorem
2007-04-20 Claudio Sacerdoti... Much ado about nothing:
2007-03-16 Andrea AspertiExtensions required for the moebius function (in Z).
2007-03-13 Andrea AspertiFew theorems added.`
2007-03-13 Andrea Aspertinew version of div_and_mod
2006-12-18 Andrea AspertiRenamed iterative into map_iter_p and moved around...
2006-12-18 Andrea AspertiProof of Euler theorem.
2006-11-27 Andrea AspertiSmall changes
2006-11-23 Andrea AspertiMinor changes.
2006-11-15 Ferruccio Guidifixed base uri
2006-11-15 Andrea AspertiAdded lt_O_S.
2006-10-30 Andrea Aspertilibrary = yes!
2006-10-25 Claudio Sacerdoti... Our unification used to guess a very complex argument...
2006-10-09 Claudio Sacerdoti... added to applyS in nat/gcd.ma a timeout large enough...
2006-10-06 Enrico Tassiresumed ol auto
2006-10-03 Enrico Tassicommented out are_convertible in is_identity
2006-10-02 Enrico Tassiremoved a pointless call to auto
2006-09-29 Enrico Tassirestored the good factorization file
2006-09-27 Claudio Sacerdoti... Initial work on setoids:
2006-09-21 Enrico Tassiauto snapshot
2006-07-26 Stefano Zacchiroliadded tinycals to the proof we frequently use for examp...
2006-07-24 Andrea AspertiA compiling version of the library.
2006-07-24 Stefano Zacchiroliadded missing dependency
next