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

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

[helm.git] / helm / software / matita / nlibrary / algebra / magmas.ma

2009-09-08	Enrico Tassi	snapshot for CSC	blob \| commitdiff \| raw
2009-08-06	Claudio Sacerdoti...	Hmmm: I don't see much gain here.	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-04	Claudio Sacerdoti...	Hmmm, quite broken now.	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...	napply now automatically inserts \ldots at the end	blob \| commitdiff \| raw \| diff to current
2009-07-30	Claudio Sacerdoti...	More \ldots.	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-24	Claudio Sacerdoti...	It works better now.	blob \| commitdiff \| raw \| diff to current
2009-07-24	Claudio Sacerdoti...	No more hand-made coercions.	blob \| commitdiff \| raw \| diff to current
2009-07-23	Claudio Sacerdoti...	...	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-21	Claudio Sacerdoti...	Record projections are now automatically generated...	blob \| commitdiff \| raw \| diff to current
2009-07-20	Claudio Sacerdoti...	nrewrite now working	blob \| commitdiff \| raw \| diff to current
2009-07-13	Claudio Sacerdoti...	First proof finished (some tactics still not working).	blob \| commitdiff \| raw \| diff to current
2009-07-13	Claudio Sacerdoti...	Coercion hiding implemented. Notes:	blob \| commitdiff \| raw \| diff to current
2009-07-10	Claudio Sacerdoti...	Composite coercions are here!	blob \| commitdiff \| raw \| diff to current
2009-07-10	Claudio Sacerdoti...	Coercions used here and there.	blob \| commitdiff \| raw \| diff to current
2009-07-09	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	eq moved to CProp	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	Hmmmm. This way we need "canonical structures" also...	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current

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

RSS Atom