X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fdepends;h=81e17aafc7be49b91fca074e2c7ceb3e96f460b6;hb=9ab344f51ce85e260450b4065125e27e4c078c1f;hp=1fe102822c2a21e267b97e7eb638dad6f7b17ffb;hpb=acdfb53f9e12dd800bccb3aa2042e33d4bc61fce;p=helm.git

diff --git a/helm/software/matita/dama/depends b/helm/software/matita/dama/depends
index 1fe102822..81e17aafc 100644
--- a/helm/software/matita/dama/depends
+++ b/helm/software/matita/dama/depends
@@ -10,9 +10,11 @@ constructive_connectives.ma logic/connectives.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
 Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma
 lattice.ma excess.ma
 constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma
+infsup.ma sandwich_corollary.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