]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
nat model ported to the dualized version, but not itself dualized dedekind-sig-compl...
[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_dedekind_sigma_complete.ma
2008-10-20 Enrico Tassinat model ported to the dualized version, but not itsel...
2008-07-15 Enrico Tassimore notation moved to core notation, unification of...
2008-07-15 Enrico TassiSince CProp_i = Type_i everything lowered without 2...
2008-07-15 Enrico Tassimodels over N fixed
2008-07-07 Enrico Tassisimplified coercDb implementation with additional info...
2008-06-30 Enrico Tassisome more work on q
2008-06-24 Enrico Tassinotation factored, coercion commant taking terms and...
2008-06-19 Claudio Sacerdoti... - notation fixed according to the new stricter semantics
2008-06-17 Enrico Tassigeneral reorganization and first (unconditional) proof...