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

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

diff --git a/helm/software/matita/contribs/dama/dama/extra.ma b/helm/software/matita/contribs/dama/dama/extra.ma
index d36e0db7e165d9e1be7aeb1f827b4fc43959999a..008d84202c8b759211aae7906df041056b78491e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/extra.ma
+++ b/helm/software/matita/contribs/dama/dama/extra.ma
@@ -20,7 +20,7 @@ definition strong_ext ≝ λA:bishop_set.λop:A→A.∀x,y. op x # op y → x #
 
 definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
 
-interpretation "ordered sets less than" 'lt a b = (cic:/matita/dama/excess/lt.con _ a b).
+interpretation "ordered sets less than" 'lt a b = (lt _ a b).
 
 lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
 intros 2 (E x); intro H; cases H (_ ABS); 
@@ -51,9 +51,9 @@ intros (A x y z E H); split; cases H;
 qed.
 
 notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (cic:/matita/dama/excess/lt_rewl.con _ _ _).
+interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
 notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/excess/lt_rewr.con _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
 
 lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
 intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]