X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fdepends;fp=matita%2Fdama%2Fdepends;h=a047fc9d110a1b06e173fd892edf6959897bd3fb;hb=8080b59026efcb6461512e5122fe94c03849d06d;hp=0000000000000000000000000000000000000000;hpb=46ee5e37b7dc37d09e90c08eaa818e10f87a7ed1;p=helm.git diff --git a/matita/dama/depends b/matita/dama/depends new file mode 100644 index 000000000..a047fc9d1 --- /dev/null +++ b/matita/dama/depends @@ -0,0 +1,40 @@ +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 +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 +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 +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 +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 +classical_pointwise/sets.ma logic/connectives.ma nat/nat.ma +classical_pointfree/ordered_sets.ma excess.ma +classical_pointfree/ordered_sets2.ma classical_pointfree/ordered_sets.ma +attic/fields.ma attic/rings.ma +attic/reals.ma attic/ordered_fields_ch0.ma +attic/integration_algebras.ma attic/vector_spaces.ma lattice.ma +attic/vector_spaces.ma attic/reals.ma +attic/rings.ma group.ma +attic/ordered_fields_ch0.ma group.ma attic/fields.ma ordered_group.ma +nat/nat.ma +logic/connectives.ma +higher_order_defs/relations.ma +Q/q.ma +nat/plus.ma +higher_order_defs/relations.ma +logic/connectives.ma +nat/orders.ma +nat/times.ma +nat/orders.ma +nat/orders.ma +nat/plus.ma +nat/orders.ma