]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/library/nat
- transcript: we have now two styles of mma's from grafite:
[helm.git] / helm / software / matita / library / nat /
2009-04-22 Enrico Tassidemodulate takes an extra argument 'all', if present...
2009-04-20 Enrico Tassi- init_cache_and_tables rewritten using the automation_...
2009-04-15 Ferruccio Guidi- transcript: bugfix
2009-03-16 Andrea AspertiAdapted to new applyS.
2009-03-16 Andrea AspertiAdded a property.
2009-02-16 Enrico Tassisome notational experiments
2009-02-13 Wilmer RicciottiAxiomatization of real numbers (work in progress)
2009-01-28 Enrico Tassi...
2008-12-19 Enrico Tassifix exponentiation
2008-08-16 Enrico Tassiadded interpretation for \naturals, \rationals, and...
2008-07-10 Enrico Tassimore work on dama
2008-06-30 Enrico Tassisome more work on q
2008-06-19 Enrico Tassinotation on steroids: 'term 40 x' is a valid variable...
2008-06-13 Claudio Sacerdoti... New lemma
2008-06-12 Enrico TassiTesting some performance tricks by caching the list...
2008-06-11 Claudio Sacerdoti... New, much faster implementation of factorize.
2008-06-09 Claudio Sacerdoti... Most of the time, URIs can now be replaced with identif...
2008-06-08 Claudio Sacerdoti... generalize no more required before elim
2008-06-08 Claudio Sacerdoti... generalize no more required before elim
2008-06-08 Claudio Sacerdoti... generalize no more required before elim
2008-06-08 Claudio Sacerdoti... generalize no more required before elim
2008-06-06 Andrea AspertiA new theorem
2008-06-06 Andrea Asperticleanup
2008-06-06 Andrea AspertiCleanup.
2008-06-06 Claudio Sacerdoti... sieve.ma now depends only on primes.ma
2008-06-05 Claudio Sacerdoti... Eratosthene's sieve factorized out of nat/bertrand...
2008-05-30 Enrico Tassigarbage removed
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...
next