Most of the time, URIs can now be replaced with identifiers in "interpretation".

[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 b5b4d8e78beb6d10f471710baa79591d7532cffd..c161fee4589d50ef1789a6968780fda804dfd2b9 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -22,17 +22,14 @@ record ordered_set: Type ≝ {
   os_cotransitive: cotransitive ? os_excess 
 }.
 
-interpretation "Ordered set excess" 'nleq a b = 
-  (cic:/matita/dama/ordered_set/os_excess.con _ a b). 
+interpretation "Ordered set excess" 'nleq a b = (os_excess _ a b). 
 
 (* Definition 2.2 (3) *)
 definition le ≝ λE:ordered_set.λa,b:E. ¬ (a ≰ b).
 
-interpretation "Ordered set greater or equal than" 'geq a b = 
- (cic:/matita/dama/ordered_set/le.con _ b a).
+interpretation "Ordered set greater or equal than" 'geq a b = (le _ b a).
 
-interpretation "Ordered set less or equal than" 'leq a b = 
- (cic:/matita/dama/ordered_set/le.con _ a b).
+interpretation "Ordered set less or equal than" 'leq a b = (le _ a b).
 
 lemma le_reflexive: ∀E.reflexive ? (le E).
 unfold reflexive; intros 3 (E x H); apply (os_coreflexive ?? H);
@@ -51,5 +48,3 @@ cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
 cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]
 cases (Lb1b H1);
 qed.
-  
-  
\ No newline at end of file