X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fclassical_pointfree%2Fordered_sets.ma;fp=matita%2Fdama%2Fclassical_pointfree%2Fordered_sets.ma;h=2630da77c6474b93a99281982f1edc229ff27ae8;hb=db068aa35cc47bb881ec810bf3b904c3d7cc9379;hp=5d9c2da67132640b6d46720aaf9e8f34f5fd7488;hpb=df666eb58afe0b312a2c4d41683d7ae4828ee8bd;p=helm.git

diff --git a/matita/dama/classical_pointfree/ordered_sets.ma b/matita/dama/classical_pointfree/ordered_sets.ma
index 5d9c2da67..2630da77c 100644
--- a/matita/dama/classical_pointfree/ordered_sets.ma
+++ b/matita/dama/classical_pointfree/ordered_sets.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/".
+
 
 include "excess.ma".
 
@@ -320,10 +320,10 @@ notation "hvbox(〈a〉)"
 for @{ 'hide_everything_but $a }.
 
 interpretation "mk_bounded_above_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 interpretation "mk_bounded_below_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 theorem eq_f_sup_sup_f:
  ∀O':dedekind_sigma_complete_ordered_set.