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

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

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

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-06	Andrea Asperti	Added frac.ma	tree \| commitdiff
2008-06-06	Andrea Asperti	Added Qplus_andrea.ma	tree \| commitdiff
2008-06-05	Claudio Sacerdoti...	Eratosthene's sieve factorized out of nat/bertrand...	tree \| commitdiff
2008-06-03	Claudio Sacerdoti...	Some proofs on enumerator and denominator.	tree \| commitdiff
2008-06-03	Claudio Sacerdoti...	More work on rational numbers with unique representations.	tree \| commitdiff
2008-05-30	Enrico Tassi	garbage removed	tree \| commitdiff
2008-05-29	Enrico Tassi	case not unfilding fixed	tree \| commitdiff
2008-05-27	Enrico Tassi	CoRN moved in contribs	tree \| commitdiff
2008-05-27	Enrico Tassi	auto calls cleanup\	tree \| commitdiff
2008-05-26	Enrico Tassi	new, more rigid syntax, for auto_params affecting the...	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-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-05-18	Claudio Sacerdoti...	Dummy dependent products in inductive types arities...	tree \| commitdiff
2008-04-11	Enrico Tassi	more fix removed from types	tree \| commitdiff
2008-04-11	Enrico Tassi	more fix removed from types in proofs	tree \| commitdiff
2008-04-11	Enrico Tassi	added a simplify to prevent the generation of an ugly fix	tree \| commitdiff
2008-04-08	Enrico Tassi	added simplify to avoid ugly proofterm	tree \| commitdiff
2008-04-02	Enrico Tassi	removed dummy rewrite	tree \| commitdiff
2008-04-02	Enrico Tassi	removed dummy rewrite	tree \| commitdiff
2008-04-02	Enrico Tassi	removed dummy rewrites	tree \| commitdiff
2008-04-02	Enrico Tassi	fixed according to the new rewrite semantics (fails...	tree \| commitdiff
2008-04-02	Enrico Tassi	fixed depends after the removal of Fsub	tree \| commitdiff
2008-03-27	Wilmer Ricciotti	Updated depedencies.	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-23	Enrico Tassi	Fsub moved in contribs	tree \| commitdiff
2008-03-22	Enrico Tassi	freescale moved under contribs. contribs made relocatable	tree \| commitdiff
2008-03-20	Claudio Sacerdoti...	Script fixed (it did not compile due to a mistake befor...	tree \| commitdiff
2008-03-20	Enrico Tassi	changed auto_tac params type and all derivate tactics...	tree \| commitdiff
2008-03-14	Claudio Sacerdoti...	Tests enabled again.	tree \| commitdiff
2008-03-13	Claudio Sacerdoti...	New version of freescale:	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-09	Claudio Sacerdoti...	Scripts fixed. They were broken since the change to...	tree \| commitdiff
2008-03-06	Enrico Tassi	* please let the library in shape *	tree \| commitdiff
2008-03-06	Enrico Tassi	fixed	tree \| commitdiff
2008-03-06	Enrico Tassi	fixed deps	tree \| commitdiff
2008-03-06	Enrico Tassi	reworked freescale stuff to put \m as a left parameter	tree \| commitdiff
2008-03-04	Claudio Sacerdoti...	New syntax for patterns.	tree \| commitdiff
2008-03-04	Claudio Sacerdoti...	prodT ==> prod	tree \| commitdiff
2008-03-04	Claudio Sacerdoti...	A) New version.	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-08	Claudio Sacerdoti...	A formalization of modified realisability with truth...	tree \| commitdiff
2008-02-08	Claudio Sacerdoti...	prodT merged with prod	tree \| commitdiff
2008-02-07	Claudio Sacerdoti...	ProdT was a perfect copy of Prod. Removed.	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-21	Claudio Sacerdoti...	Old tiny freescale experiment get rid of.	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
2008-01-11	Enrico Tassi	increased timout	tree \| commitdiff
2008-01-11	Enrico Tassi	increased a timeout, matitac (not .opt) should be able...	tree \| commitdiff
2008-01-10	Enrico Tassi	BIG FAT WARNING: DEVELOPMENTS DIE HERE	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-11-15	Enrico Tassi	autobatch => [auto]	tree \| commitdiff
2007-11-12	Ferruccio Guidi	- destruct tactic: automatic simplification in case...	tree \| commitdiff
2007-11-08	Enrico Tassi	ported to the new destruct	tree \| commitdiff
2007-11-06	Ferruccio Guidi	new implementation of the destruct tactic,	tree \| commitdiff
2007-10-28	Claudio Sacerdoti...	Nil => nil, Cons => cons	tree \| commitdiff
2007-10-28	Claudio Sacerdoti...	Nil => nil; Cons => cons	tree \| commitdiff
2007-10-28	Claudio Sacerdoti...	New syntax for match patterns.	tree \| commitdiff
next

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

RSS Atom