X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fdepends;h=8334fa1a3ba9b5d9ca5643ff3d1c322a74dfc5d7;hb=9483f7e6c85ec11f88bdb219b2cebad2039b1a74;hp=e96472aa927e914fa867866ead5bb99728b55229;hpb=196d60526aaf4a10d0eaaf79cf8919c108b27a10;p=helm.git diff --git a/helm/software/matita/dama/depends b/helm/software/matita/dama/depends index e96472aa9..8334fa1a3 100644 --- a/helm/software/matita/dama/depends +++ b/helm/software/matita/dama/depends @@ -1,21 +1,23 @@ -metric_lattice.ma excess.ma lattice.ma metric_space.ma +metric_lattice.ma lattice.ma metric_space.ma metric_space.ma ordered_divisible_group.ma -sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma sequence.ma +sandwich.ma nat/orders.ma nat/plus.ma tend.ma premetric_lattice.ma lattice.ma metric_space.ma ordered_group.ma group.ma divisible_group.ma group.ma nat/orders.ma ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma -sequence.ma excess.ma nat/orders.ma ordered_group.ma +sequence.ma excess.ma constructive_connectives.ma logic/connectives.ma lattice.TF.ma excess.ma lattice.ma nat/nat.ma group.ma excess.ma prevalued_lattice.ma ordered_group.ma excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma -sandwich_corollary.ma metric_lattice.ma sandwich.ma +sandwich_corollary.ma sandwich.ma Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma +limit.ma excess.ma infsup.ma tend.ma lattice.ma excess.ma +tend.ma metric_lattice.ma nat/orders.ma sequence.ma constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma -infsup.ma sandwich_corollary.ma +infsup.ma excess.ma sequence.ma constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma classical_pointwise/topology.ma classical_pointwise/sets.ma classical_pointwise/sigma_algebra.ma classical_pointwise/topology.ma