X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fsupremum.ma;h=2ce417ecce9398a7e9405ce347ae65ff15772718;hb=8d961585c4ff785d558d5b4c84adf656595ca487;hp=0de61b292fcaca3e40f5b7bddfa7ba0b88d27398;hpb=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git

diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma
index 0de61b292..2ce417ecc 100644
--- a/helm/software/matita/library/dama/supremum.ma
+++ b/helm/software/matita/library/dama/supremum.ma
@@ -15,8 +15,8 @@
 
 include "datatypes/constructors.ma".
 include "nat/plus.ma".
-include "nat_ordered_set.ma".
-include "sequence.ma".
+include "dama/nat_ordered_set.ma".
+include "dama/sequence.ma".
 
 (* Definition 2.4 *)
 definition upper_bound ≝ 
@@ -121,7 +121,7 @@ interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l
 interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
 
 lemma hint_nat :
- Type_of_ordered_set nat_ordered_set →
+ Type_OF_ordered_set nat_ordered_set →
    hos_carr (os_l (nat_ordered_set)).
 intros; assumption;
 qed.