]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0b15dfd) | patch
Since CProp_i = Type_i everything lowered without 2 distinct Sigma.
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Jul 2008 12:01:23 +0000 (12:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Jul 2008 12:01:23 +0000 (12:01 +0000)
commita99ab6bf4e5bb993d363a9e62985371ba14cf71a
tree4b00446bd37ca96d9ca8152e04a2f03934eaed11tree | snapshot
parent0b15dfdee3357a626c77d30599e87a83ab34e471commit | diff
Since CProp_i = Type_i everything lowered without 2 distinct Sigma.
helm/software/matita/contribs/dama/dama/cprop_connectives.ma diff | blob | history
helm/software/matita/contribs/dama/dama/lebesgue.ma diff | blob | history
helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma diff | blob | history
helm/software/matita/contribs/dama/dama/ordered_uniform.ma diff | blob | history
helm/software/matita/contribs/dama/dama/property_sigma.ma diff | blob | history
helm/software/matita/contribs/dama/dama/supremum.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.