]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/nlibrary/sets
Use the inversion!
[helm.git] / helm / software / matita / nlibrary / sets /
2010-03-02 Wilmer RicciottiSome integrations to the ng library.
2010-02-03 Claudio Sacerdoti... Curryfication of binary setoids.
2010-02-03 Claudio Sacerdoti... Curryfication of binary morphisms.
2010-02-03 Claudio Sacerdoti... Work in Progress: Who needs binary_morphisms? Curryfica...
2010-01-18 Claudio Sacerdoti... More // everywhere.
2010-01-18 Claudio Sacerdoti... // used everywhere!
2010-01-18 Claudio Sacerdoti... // in place of nauto everywhere
2010-01-02 Claudio Sacerdoti... 1) stuff moved from categories.ma to setoids*.ma
2009-12-30 Claudio Sacerdoti... Porting of Sambin's stuff started.
2009-12-30 Claudio Sacerdoti... ...
2009-10-28 Claudio Sacerdoti... Different aliases, better equality inferred.
2009-10-28 Claudio Sacerdoti... instances
2009-10-23 Claudio Sacerdoti... Alias required now ??
2009-10-16 Enrico Tassi...
2009-10-06 Enrico Tassisome fixes
2009-10-05 Claudio Sacerdoti... ...
2009-10-05 Claudio Sacerdoti... ...
2009-10-05 Enrico Tassiuffa
2009-10-04 Claudio Sacerdoti... Does not compile! Wrong unification hint?
2009-10-04 Claudio Sacerdoti... ...
2009-10-02 Enrico Tassihints fixed
2009-09-30 Claudio Sacerdoti... With this hint, it diverges.
2009-09-29 Claudio Sacerdoti... ...
2009-09-29 Enrico Tassi...
2009-09-29 Claudio Sacerdoti... It does not work recursively...
2009-09-29 Claudio Sacerdoti... ...
2009-09-28 Enrico Tassinon ho resistito!
2009-09-28 Claudio Sacerdoti... Experiment...
2009-09-21 Enrico Tassihuge commit regarding universes:
2009-09-18 Claudio Sacerdoti... ...
2009-09-16 Enrico Tassisome more work...
2009-09-16 Claudio Sacerdoti... New interesting coercion.
2009-09-15 Enrico Tassiimproved check in delift for flexible lc entries.
2009-09-14 Enrico Tassifixed coercion mechanism w.r.t. undo/require
2009-09-14 Claudio Sacerdoti... New tactics ncut and nlapply.
2009-09-11 Enrico Tassiconstructor accepts the arguments of the constructor...
2009-09-10 Enrico Tassiok, but slow on includes
2009-09-10 Enrico Tassinice hints
2009-09-10 Enrico Tassiit starts to work
2009-09-10 Enrico Tassimore stuff fixed
2009-09-08 Enrico Tassisnapshot for CSC
2009-08-24 Claudio Sacerdoti... Nicer proof "finished" (up to arithmetical facts).
2009-08-21 Claudio Sacerdoti... Towards a simplified proof.
2009-08-21 Claudio Sacerdoti... ...
2009-08-20 Claudio Sacerdoti... Injectivity proved! What a mess...
2009-08-20 Claudio Sacerdoti... ...
2009-08-20 Claudio Sacerdoti... - Bug fixed in definition of big_op.
2009-08-20 Claudio Sacerdoti... ...
2009-08-19 Claudio Sacerdoti... One half done.
2009-08-19 Claudio Sacerdoti... ...
2009-08-18 Claudio Sacerdoti... ...
2009-08-18 Claudio Sacerdoti... ...
2009-08-18 Claudio Sacerdoti... ...
2009-08-14 Claudio Sacerdoti... ...
2009-08-14 Claudio Sacerdoti... ...
2009-08-12 Claudio Sacerdoti... A very little bit of arithmetic.
2009-08-06 Claudio Sacerdoti... The first omomorphism theorem for whole sets (i.e....
2009-08-06 Claudio Sacerdoti... Setoid rewriting as unification hinting. Does not work...
2009-08-04 Claudio Sacerdoti... More Gonthierism. Are they the right solution?
2009-08-04 Claudio Sacerdoti... ...
2009-08-01 Claudio Sacerdoti... Smaller formulae.
2009-07-31 Claudio Sacerdoti... Setoids, setoids1, sets, and the like. The mess begins.
2009-07-31 Claudio Sacerdoti... Record projections are now defined as fixpoints in...
2009-07-30 Claudio Sacerdoti... More napply \ldots => napply
2009-07-30 Claudio Sacerdoti... More \ldots.
2009-07-30 Claudio Sacerdoti... \ldots used here and there. Cool!
2009-07-27 Claudio Sacerdoti... setoids.ma split into setoids.ma + setoids1.ma
2009-07-27 Claudio Sacerdoti... topology/igt.ma (???) |-> sets/setoids.ma
2009-07-21 Claudio Sacerdoti... 1) record projections are now automatically generated
2009-07-08 Claudio Sacerdoti... ...
2009-07-07 Claudio Sacerdoti... ...
2009-07-07 Claudio Sacerdoti... Let's play a bit with NG.