matita.cs.unibo.it Git - helm.git/history - helm/software/matita/library/nat

]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/library/nat

[helm.git] / helm / software / matita / library / nat /

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
2007-06-26	Cristian Armentano	(no commit message)	tree \| commitdiff
2007-06-26	Cristian Armentano	generic sommatory.	tree \| commitdiff
2007-05-24	Enrico Tassi	auto and autogui... some work	tree \| commitdiff
2007-05-17	Enrico Tassi	auto rewritten with only one tail recursive function.	tree \| commitdiff
2007-05-09	Andrea Asperti	A few extensions for the moebius inversion theorem	tree \| commitdiff
2007-04-20	Claudio Sacerdoti...	Much ado about nothing:	tree \| commitdiff
2007-03-16	Andrea Asperti	Extensions required for the moebius function (in Z).	tree \| commitdiff
2007-03-13	Andrea Asperti	Few theorems added.`	tree \| commitdiff
2007-03-13	Andrea Asperti	new version of div_and_mod	tree \| commitdiff
next

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom