]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/contribs
Some work on concrete spaces.
[helm.git] / helm / software / matita / contribs /
2009-01-06 Claudio Sacerdoti... Some work on concrete spaces.
2009-01-06 Claudio Sacerdoti... Cool: only 8 universes in use.
2009-01-06 Claudio Sacerdoti... 1) Some reorganization.
2009-01-06 Claudio Sacerdoti... Some renaming to avoid confusion between saturations...
2009-01-06 Claudio Sacerdoti... Fixing universe levels for saturations and (partially...
2009-01-06 Claudio Sacerdoti... The functor from BP to OBP has been defined (but no...
2009-01-06 Claudio Sacerdoti... Ok, even if not stated formally, now we know that the...
2009-01-06 Claudio Sacerdoti... orelation_of_relation preserves equality and identities.
2009-01-06 Claudio Sacerdoti... Basic pairs restored; require renaming to use them...
2009-01-06 Claudio Sacerdoti... Some progress: everything works well now.
2009-01-06 Claudio Sacerdoti... Ooops, I forgot to commit this in the previous 3-4...
2009-01-06 Claudio Sacerdoti... An hint moved to the right place.
2009-01-06 Claudio Sacerdoti... No more daemons, no more exTs.
2009-01-06 Claudio Sacerdoti... Great: some significant progress in fixing universe...
2009-01-04 Claudio Sacerdoti... ...
2009-01-04 Claudio Sacerdoti... 1. CProp_n fixed to be equal to Type_n to better unders...
2009-01-04 Claudio Sacerdoti... Snapshot to try to understand something.
2009-01-04 Claudio Sacerdoti... Some more progress, fighting universe inconsistencies.
2009-01-04 Claudio Sacerdoti... Yet another universe problem :-(
2009-01-04 Claudio Sacerdoti... ...
2009-01-04 Claudio Sacerdoti... Back to step 1: all files that used to pass now pass...
2009-01-04 Claudio Sacerdoti... More re-organization.
2009-01-03 Claudio Sacerdoti... Basic pairs went through with no problems.
2009-01-03 Claudio Sacerdoti... Universe level fixed (litterally).
2009-01-03 Claudio Sacerdoti... Niceness was just a temporary illusion :-(
2009-01-03 Claudio Sacerdoti... Much, much nicer now.
2009-01-03 Claudio Sacerdoti... Some more re-organization.
2009-01-03 Claudio Sacerdoti... More re-working.
2009-01-03 Claudio Sacerdoti... More reorganization.
2008-12-28 Claudio Sacerdoti... equivalence_relations made uniform w.r.t. universe...
2008-12-28 Claudio Sacerdoti... Final work for today.
2008-12-28 Enrico Tassiremoved duplicate notation
2008-12-28 Claudio Sacerdoti... Some more painful work.
2008-12-28 Claudio Sacerdoti... binary_meet is back again, with some effort
2008-12-28 Claudio Sacerdoti... Many universe inconsistency avoided here and there.
2008-12-28 Claudio Sacerdoti... The universe inconsistency comes from big union, that...
2008-12-28 Claudio Sacerdoti... Proof that \Omega \sup A is an overlap algebra, up...
2008-12-28 Claudio Sacerdoti... o-algebra defined again
2008-12-28 Claudio Sacerdoti... Categories and subsets compile again, hopefully with...
2008-12-28 Claudio Sacerdoti... WARNING: partial commit to try to understand something.
2008-12-26 Claudio Sacerdoti... Some more fixes. Boring and stupid!
2008-12-26 Claudio Sacerdoti... Some fixes.
2008-12-26 Claudio Sacerdoti... O-Basic Topologies do form a category.
2008-12-26 Claudio Sacerdoti... A few more lines.
2008-12-26 Claudio Sacerdoti... Some notes by Giovanni.
2008-12-26 Claudio Sacerdoti... Some notes by Giovanni.
2008-12-22 Claudio Sacerdoti... Just copied here from formal_topologies.ma.
2008-12-22 Claudio Sacerdoti... More (ugly) work.
2008-12-22 Enrico Tassi...
2008-12-22 Enrico TassiBeginning of o-basic_topologies.
2008-12-22 Enrico TassiSome clean up.
2008-12-22 Enrico TassiConcrete Spaces defined but... they require about 20m...
2008-12-22 Enrico Tassi1 more lemma
2008-12-22 Enrico Tassione line
2008-12-22 Enrico Tassisome work
2008-12-22 Claudio Sacerdoti... ums got rid of
2008-12-21 Claudio Sacerdoti... 1) no more DAEMONS
2008-12-21 Enrico Tassimerged commits, the same proof is missing :-(
2008-12-21 Enrico Tassibleah
2008-12-21 Claudio Sacerdoti... Using the new category SET.
2008-12-19 Enrico Tassi...
2008-12-19 Enrico Tassigo notation go!
2008-12-18 Claudio Sacerdoti... Many axioms are now proved... using many more (but...
2008-12-17 Enrico Tassifoo overlap
2008-12-17 Enrico Tassifoo overlap
2008-12-17 Enrico Tassi....
2008-12-14 Enrico Tassi...
2008-12-12 Claudio Sacerdoti... ...
2008-12-12 Claudio Sacerdoti... A parser (and a scanner) to import "~C" files into...
2008-12-12 Claudio Sacerdoti... ...
2008-12-12 Claudio Sacerdoti... 1. new expressions AND, OR, XOR
2008-12-12 Enrico Tassithanks to the new fixes to notation, I can define ...
2008-12-05 Claudio Sacerdoti... Case-sensitive fixes.
2008-11-28 Ferruccio GuidicicDischarge: final fixup. Now correctly processes...
2008-11-25 Ferruccio GuidicicUtil: we moved here pp_term from proceduralHelpers
2008-11-24 Enrico Tassi...
2008-11-24 Enrico Tassiformal topologies
2008-11-20 Enrico Tassi...
2008-11-20 Enrico Tassi...
2008-11-19 Enrico Tassix2sx declared as coercion and used when possible
2008-11-19 Enrico Tassirenaming
2008-11-19 Enrico Tassi...
2008-11-15 Enrico Tassihousekeeping
2008-11-15 Enrico Tassihousekeeping
2008-11-12 Enrico Tassibetter names
2008-11-11 Enrico Tassilast fixes
2008-11-11 Claudio Sacerdoti... 1. data structure for lables is now more strict
2008-11-07 Enrico Tassisome other simplification
2008-11-07 Enrico Tassiordered_set simplified
2008-11-07 Enrico Tassiexercise ready
2008-11-06 Enrico Tassiexercise ready
2008-11-06 Enrico Tassialmost there
2008-11-06 Claudio Sacerdoti... ...
2008-11-06 Claudio Sacerdoti... First attempts at the third phase.
2008-11-06 Enrico Tassialmost ok
2008-11-06 Enrico Tassifixed scripts
2008-11-05 Enrico Tassistill some glitches, but reaching a decent state
2008-11-05 Enrico Tassiusing the new by foo we proved semantics
2008-11-04 Enrico Tassieliminazione di un passaggio di transitività in ast2astfe
2008-11-03 Enrico TassiBDD
next