matita.cs.unibo.it Git - helm.git/history - helm/software/matita/nlibrary/sets/sets.ma

]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/nlibrary/sets/sets.ma

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

2010-09-09	Enrico Tassi	th 16.2 proved in the setoids setting	blob \| commitdiff \| raw
2010-07-22	Enrico Tassi	eq -> eq0 renaming	blob \| commitdiff \| raw \| diff to current
2010-03-02	Wilmer Ricciotti	Some integrations to the ng library.	blob \| commitdiff \| raw \| diff to current
2010-02-03	Claudio Sacerdoti...	Curryfication of binary morphisms.	blob \| commitdiff \| raw \| diff to current
2010-02-03	Claudio Sacerdoti...	Work in Progress: Who needs binary_morphisms? Curryfica...	blob \| commitdiff \| raw \| diff to current
2010-01-18	Claudio Sacerdoti...	// used everywhere!	blob \| commitdiff \| raw \| diff to current
2009-10-23	Claudio Sacerdoti...	Alias required now ??	blob \| commitdiff \| raw \| diff to current
2009-10-06	Enrico Tassi	some fixes	blob \| commitdiff \| raw \| diff to current
2009-10-05	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-10-05	Enrico Tassi	uffa	blob \| commitdiff \| raw \| diff to current
2009-10-04	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-10-02	Enrico Tassi	hints fixed	blob \| commitdiff \| raw \| diff to current
2009-09-30	Claudio Sacerdoti...	With this hint, it diverges.	blob \| commitdiff \| raw \| diff to current
2009-09-29	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-09-29	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2009-09-29	Claudio Sacerdoti...	It does not work recursively...	blob \| commitdiff \| raw \| diff to current
2009-09-28	Enrico Tassi	non ho resistito!	blob \| commitdiff \| raw \| diff to current
2009-09-28	Claudio Sacerdoti...	Experiment...	blob \| commitdiff \| raw \| diff to current
2009-09-21	Enrico Tassi	huge commit regarding universes:	blob \| commitdiff \| raw \| diff to current
2009-09-16	Enrico Tassi	some more work...	blob \| commitdiff \| raw \| diff to current
2009-09-16	Claudio Sacerdoti...	New interesting coercion.	blob \| commitdiff \| raw \| diff to current
2009-09-14	Enrico Tassi	fixed coercion mechanism w.r.t. undo/require	blob \| commitdiff \| raw \| diff to current
2009-09-14	Claudio Sacerdoti...	New tactics ncut and nlapply.	blob \| commitdiff \| raw \| diff to current
2009-09-11	Enrico Tassi	constructor accepts the arguments of the constructor...	blob \| commitdiff \| raw \| diff to current
2009-09-10	Enrico Tassi	nice hints	blob \| commitdiff \| raw \| diff to current
2009-09-10	Enrico Tassi	it starts to work	blob \| commitdiff \| raw \| diff to current
2009-09-10	Enrico Tassi	more stuff fixed	blob \| commitdiff \| raw \| diff to current
2009-09-08	Enrico Tassi	snapshot for CSC	blob \| commitdiff \| raw \| diff to current
2009-08-24	Claudio Sacerdoti...	Nicer proof "finished" (up to arithmetical facts).	blob \| commitdiff \| raw \| diff to current
2009-08-18	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-08-14	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-08-12	Claudio Sacerdoti...	A very little bit of arithmetic.	blob \| commitdiff \| raw \| diff to current
2009-08-06	Claudio Sacerdoti...	The first omomorphism theorem for whole sets (i.e....	blob \| commitdiff \| raw \| diff to current
2009-08-06	Claudio Sacerdoti...	Setoid rewriting as unification hinting. Does not work...	blob \| commitdiff \| raw \| diff to current
2009-08-04	Claudio Sacerdoti...	More Gonthierism. Are they the right solution?	blob \| commitdiff \| raw \| diff to current
2009-08-04	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-08-01	Claudio Sacerdoti...	Smaller formulae.	blob \| commitdiff \| raw \| diff to current
2009-07-31	Claudio Sacerdoti...	Setoids, setoids1, sets, and the like. The mess begins.	blob \| commitdiff \| raw \| diff to current
2009-07-30	Claudio Sacerdoti...	More napply \ldots => napply	blob \| commitdiff \| raw \| diff to current
2009-07-30	Claudio Sacerdoti...	\ldots used here and there. Cool!	blob \| commitdiff \| raw \| diff to current
2009-07-21	Claudio Sacerdoti...	1) record projections are now automatically generated	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-07-07	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-07-07	Claudio Sacerdoti...	Let's play a bit with NG.	blob \| commitdiff \| raw \| diff to current

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

RSS Atom