| 2009-04-22 |
Enrico Tassi | demodulate takes an extra argument 'all', if present... |
tree | commitdiff |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_... |
tree | commitdiff |
| 2009-04-15 |
Ferruccio Guidi | - transcript: bugfix |
tree | commitdiff |
| 2009-03-16 |
Andrea Asperti | Adapted to new applyS. |
tree | commitdiff |
| 2009-03-16 |
Andrea Asperti | Added a property. |
tree | commitdiff |
| 2009-02-16 |
Enrico Tassi | some notational experiments |
tree | commitdiff |
| 2009-02-13 |
Wilmer Ricciotti | Axiomatization of real numbers (work in progress) |
tree | commitdiff |
| 2009-01-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | fix exponentiation |
tree | commitdiff |
| 2008-08-16 |
Enrico Tassi | added interpretation for \naturals, \rationals, and... |
tree | commitdiff |
| 2008-07-10 |
Enrico Tassi | more work on dama |
tree | commitdiff |
| 2008-06-30 |
Enrico Tassi | some more work on q |
tree | commitdiff |
| 2008-06-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable... |
tree | commitdiff |
| 2008-06-13 |
Claudio Sacerdoti... | New lemma |
tree | commitdiff |
| 2008-06-12 |
Enrico Tassi | Testing some performance tricks by caching the list... |
tree | commitdiff |
| 2008-06-11 |
Claudio Sacerdoti... | New, much faster implementation of factorize. |
tree | commitdiff |
| 2008-06-09 |
Claudio Sacerdoti... | Most of the time, URIs can now be replaced with identif... |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-06 |
Andrea Asperti | A new theorem |
tree | commitdiff |
| 2008-06-06 |
Andrea Asperti | cleanup |
tree | commitdiff |
| 2008-06-06 |
Andrea Asperti | Cleanup. |
tree | commitdiff |
| 2008-06-06 |
Claudio Sacerdoti... | sieve.ma now depends only on primes.ma |
tree | commitdiff |
| 2008-06-05 |
Claudio Sacerdoti... | Eratosthene's sieve factorized out of nat/bertrand... |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | garbage removed |
tree | commitdiff |
| 2008-05-27 |
Enrico Tassi | auto calls cleanup\ |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-04-02 |
Enrico Tassi | removed dummy rewrite |
tree | commitdiff |
| 2008-04-02 |
Enrico Tassi | removed dummy rewrite |
tree | commitdiff |
| 2008-03-26 |
Wilmer Ricciotti | Reorganization of list library (step 1) |
tree | commitdiff |
| 2008-03-25 |
Wilmer Ricciotti | small update |
tree | commitdiff |
| 2008-03-12 |
Claudio Sacerdoti... | Problem solved (was: apply needed an argument to avoid... |
tree | commitdiff |
| 2008-03-12 |
Andrea Asperti | Nuova dimostrazione riflessiva di le_to_Bertrand. |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Scripts fixed because of: |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | * please let the library in shape * |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | fixed |
tree | commitdiff |
| 2008-02-27 |
Wilmer Ricciotti | the proof of bertrand's conjecture is now complete |
tree | commitdiff |
| 2008-02-22 |
Wilmer Ricciotti | sieve of erathostene (proof of soundness almost done) |
tree | commitdiff |
| 2008-02-19 |
Andrea Asperti | Added o.ma (some results about the magnitude of functio... |
tree | commitdiff |
| 2008-02-18 |
Andrea Asperti | Complete proof of Bertrand for n >= 256. |
tree | commitdiff |
| 2008-02-14 |
Andrea Asperti | Prima versione di bertrand. Tanti cambiamenti qua e la. |
tree | commitdiff |
| 2008-02-08 |
Andrea Asperti | progress. |
tree | commitdiff |
| 2008-02-07 |
Andrea Asperti | Results about Chebyshev teta function. |
tree | commitdiff |
| 2008-02-05 |
Andrea Asperti | Some more theorems. |
tree | commitdiff |
| 2008-02-05 |
Wilmer Ricciotti | lower bound for neper's constant |
tree | commitdiff |
| 2008-02-04 |
Andrea Asperti | Improved approximations for A and prim. |
tree | commitdiff |
| 2008-02-04 |
Andrea Asperti | Some improvement. |
tree | commitdiff |
| 2008-01-31 |
Wilmer Ricciotti | Square root added. |
tree | commitdiff |
| 2008-01-30 |
Andrea Asperti | Improved approximations |
tree | commitdiff |
| 2008-01-29 |
Andrea Asperti | New approximtions. |
tree | commitdiff |
| 2008-01-22 |
Wilmer Ricciotti | Bertrand's conjecture (weak), some work in progress |
tree | commitdiff |
| 2008-01-15 |
Wilmer Ricciotti | update: upper bound for prim |
tree | commitdiff |
| 2008-01-14 |
Wilmer Ricciotti | Chebyshev's upper bound on prim |
tree | commitdiff |
| 2007-12-21 |
Wilmer Ricciotti | beginning proof of chebyshev's bound on prim. |
tree | commitdiff |
| 2007-12-17 |
Wilmer Ricciotti | upper bound for logarithmic summation |
tree | commitdiff |
| 2007-12-17 |
Andrea Asperti | A few more lemmas. |
tree | commitdiff |
| 2007-12-13 |
Andrea Asperti | Some inequalities. |
tree | commitdiff |
| 2007-12-12 |
Wilmer Ricciotti | Progress. |
tree | commitdiff |
| 2007-12-11 |
Andrea Asperti | Partial progress. |
tree | commitdiff |
| 2007-12-10 |
Andrea Asperti | Main result for e. |
tree | commitdiff |
| 2007-12-10 |
Andrea Asperti | Restructuring. |
tree | commitdiff |
| 2007-12-10 |
Andrea Asperti | Main inequalities for e. |
tree | commitdiff |
| 2007-12-09 |
Wilmer Ricciotti | Added summation formula for the power of a binomial. |
tree | commitdiff |
| 2007-12-07 |
Andrea Asperti | Binomial coefficients and costant e. |
tree | commitdiff |
| 2007-12-07 |
Andrea Asperti | A few more theorems. |
tree | commitdiff |
| 2007-12-03 |
Andrea Asperti | Some progress. |
tree | commitdiff |
| 2007-11-26 |
Andrea Asperti | Almost there. |
tree | commitdiff |
| 2007-11-22 |
Andrea Asperti | Big progress |
tree | commitdiff |
| 2007-11-19 |
Andrea Asperti | Towards chebyshev. |
tree | commitdiff |
| 2007-10-14 |
Claudio Sacerdoti... | Some lemmas moves to the file they belong to. |
tree | commitdiff |
| 2007-10-14 |
Cristian Armentano | Theorem sigma_p_knm changed into generic_iter_p_knm. |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-10-12 |
Andrea Asperti | More restructuring in moebius.ma |
tree | commitdiff |
| 2007-10-12 |
Andrea Asperti | Reorganization of the library. |
tree | commitdiff |
| 2007-09-20 |
Cristian Armentano | Further simplifications to the main theorem about Euler... |
tree | commitdiff |
| 2007-09-19 |
Cristian Armentano | * Some simplifications to theorem in file totient1.ma. |
tree | commitdiff |
| 2007-09-18 |
Cristian Armentano | some theorems have been moved to more appropriate files... |
tree | commitdiff |
| 2007-09-17 |
Cristian Armentano | temporary changes, before the complete cancellation... |
tree | commitdiff |
| 2007-09-17 |
Cristian Armentano | simplified version of a theorem. |
tree | commitdiff |
| 2007-09-17 |
Andrea Asperti | A new function. |
tree | commitdiff |
| 2007-09-11 |
Cristian Armentano | some theorem names changed. |
tree | commitdiff |
| 2007-09-10 |
Cristian Armentano | other simplifications. |
tree | commitdiff |
| 2007-09-09 |
Cristian Armentano | other simplifications. |
tree | commitdiff |
| 2007-09-07 |
Cristian Armentano | some simplifications. |
tree | commitdiff |
| 2007-09-06 |
Cristian Armentano | Some simplifications. |
tree | commitdiff |
| 2007-08-16 |
Cristian Armentano | little change to theorem eq_gcd_times_times_eqv_times_gcd |
tree | commitdiff |
| 2007-07-31 |
Andrea Asperti | removed generic_sigma_p since generic_iter_p is the... |
tree | commitdiff |
| 2007-07-30 |
Cristian Armentano | renamed generic_sigma_p.ma to generic_iter_p.ma |
tree | commitdiff |
| 2007-07-23 |
Claudio Sacerdoti... | Prototype of min_aux changed. |
tree | commitdiff |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
tree | commitdiff |
| 2007-06-30 |
Cristian Armentano | New definition of Euler's totient function. |
tree | commitdiff |
| 2007-06-29 |
Cristian Armentano | generic version, specializing generic_sigma_p.ma |
tree | commitdiff |
| 2007-06-29 |
Cristian Armentano | theorems about sigma_p proved using sigma_p_gen |
tree | commitdiff |
| 2007-06-27 |
Cristian Armentano | new gcd properties, and theorems for totient, and theor... |
tree | commitdiff |
| next |
projects / helm.git / history