Snapshot.

[helm.git] / helm / software / matita / contribs / dama / dama / ordered_set.ma

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index a820eff542c5a94c93843f58364883546d86ae10..45a8a1b379c1e4d866dd48a6d1c575bce6edb971 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
 (* Definition 2.1 *)
 record ordered_set: Type ≝ {
@@ -52,7 +52,7 @@ qed.
 lemma square_ordered_set: ordered_set → ordered_set.
 intro O;
 apply (mk_ordered_set (O × O));
-[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
+[1: intros (x y); apply (\fst x ≰ \fst y ∨ \snd x ≰ \snd y);
 |2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
     cases H (X X); apply (os_coreflexive ?? X);
 |3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2); 
@@ -70,7 +70,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).