X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_set.ma;h=06c222830351ef1e2820df5af1f30c3ce0663095;hb=a660b97f5a882da420809831581a7c3202fdaf35;hp=a227af3c1928927fe04185224cfe1b409d9b8029;hpb=ca41435a6021292ccba239aa173651c0be705b45;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index a227af3c1..06c222830 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -12,7 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "cprop_connectives.ma".
+include "datatypes/constructors.ma".
+include "logic/cprop_connectives.ma".
 
 (* Definition 2.1 *)
 record ordered_set: Type ≝ {
@@ -70,7 +71,5 @@ interpretation "ordered set square" 'square_os s = (square_ordered_set s).
 
 definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
 
-notation "a \subseteq u" left associative with precedence 70 
-  for @{ 'subset $a $u }.
-interpretation "ordered set subset" 'subset a b = (os_subset _ a b). 
+interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b).