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-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
2006-12-18	Andrea Asperti	Renamed iterative into map_iter_p and moved around...	tree \| commitdiff
2006-12-18	Andrea Asperti	Proof of Euler theorem.	tree \| commitdiff
2006-11-27	Andrea Asperti	Small changes	tree \| commitdiff
2006-11-23	Andrea Asperti	Minor changes.	tree \| commitdiff
2006-11-15	Ferruccio Guidi	fixed base uri	tree \| commitdiff
2006-11-15	Andrea Asperti	Added lt_O_S.	tree \| commitdiff
2006-10-30	Andrea Asperti	library = yes!	tree \| commitdiff
2006-10-25	Claudio Sacerdoti...	Our unification used to guess a very complex argument...	tree \| commitdiff
2006-10-09	Claudio Sacerdoti...	added to applyS in nat/gcd.ma a timeout large enough...	tree \| commitdiff
2006-10-06	Enrico Tassi	resumed ol auto	tree \| commitdiff
2006-10-03	Enrico Tassi	commented out are_convertible in is_identity	tree \| commitdiff
2006-10-02	Enrico Tassi	removed a pointless call to auto	tree \| commitdiff
2006-09-29	Enrico Tassi	restored the good factorization file	tree \| commitdiff
2006-09-27	Claudio Sacerdoti...	Initial work on setoids:	tree \| commitdiff
2006-09-21	Enrico Tassi	auto snapshot	tree \| commitdiff
2006-07-26	Stefano Zacchiroli	added tinycals to the proof we frequently use for examp...	tree \| commitdiff
2006-07-24	Andrea Asperti	A compiling version of the library.	tree \| commitdiff
2006-07-24	Stefano Zacchiroli	added missing dependency	tree \| commitdiff
next

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

RSS Atom