maction support added to notation, adopted for = AKA = \sub t

[helm.git] / helm / software / matita / library / dama / supremum.ma

diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma
index 0de61b292fcaca3e40f5b7bddfa7ba0b88d27398..2ce417ecce9398a7e9405ce347ae65ff15772718 100644 (file)
--- 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.