X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fbishop_set_rewrite.ma;h=7ead93370f36a5609c6839b4d80c25ef979d4f91;hb=b12a46d53cf80d40b253ca5dd495397c5c0b4287;hp=19518a67b6f29eb593a177f8d7817aba5863ea6e;hpb=6b843ebfba2ed19d2bf7a564a9d2fc92da880169;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
index 19518a67b..7ead93370 100644
--- a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
@@ -22,8 +22,7 @@ lemma eq_trans:∀E:bishop_set.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝
 notation > "'Eq'≈" non associative with precedence 50 
   for @{'eqrewrite}.
   
-interpretation "eq_rew" 'eqrewrite = 
-  (cic:/matita/dama/bishop_set/eq_trans.con _ _ _).
+interpretation "eq_rew" 'eqrewrite = (eq_trans _ _ _).
 
 lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
 intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
@@ -36,9 +35,9 @@ intro Xyz; apply Exy; left; assumption;
 qed.
 
 notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
-interpretation "le_rewl" 'lerewritel = (cic:/matita/dama/bishop_set_rewrite/le_rewl.con _ _ _).
+interpretation "le_rewl" 'lerewritel = (le_rewl _ _ _).
 notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
-interpretation "le_rewr" 'lerewriter = (cic:/matita/dama/bishop_set_rewrite/le_rewr.con _ _ _).
+interpretation "le_rewr" 'lerewriter = (le_rewr _ _ _).
 
 lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
 intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
@@ -51,9 +50,9 @@ apply bs_symmetric; assumption;
 qed.
 
 notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
-interpretation "ap_rewl" 'aprewritel = (cic:/matita/dama/bishop_set_rewrite/ap_rewl.con _ _ _).
+interpretation "ap_rewl" 'aprewritel = (ap_rewl _ _ _).
 notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
-interpretation "ap_rewr" 'aprewriter = (cic:/matita/dama/bishop_set_rewrite/ap_rewr.con _ _ _).
+interpretation "ap_rewr" 'aprewriter = (ap_rewr _ _ _).
 
 lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
 intros (A x z y Exy Ayz); cases (os_cotransitive ??? x Ayz); [2:assumption]
@@ -66,9 +65,9 @@ cases (Exy); left; assumption;
 qed.
 
 notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.
-interpretation "exc_rewl" 'ordered_setrewritel = (cic:/matita/dama/bishop_set_rewrite/exc_rewl.con _ _ _).
+interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl _ _ _).
 notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
-interpretation "exc_rewr" 'ordered_setrewriter = (cic:/matita/dama/bishop_set_rewrite/exc_rewr.con _ _ _).
+interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr _ _ _).
 
 
 lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
@@ -82,7 +81,7 @@ 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/bishop_set_rewrite/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/bishop_set_rewrite/lt_rewr.con _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).