X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fformal_topology2.ma;h=10666ba35d010c169827c24266cacc099e1444fa;hb=275b124e484510dc49141f86b5174f8bd0be7d97;hp=b98865a5cf1b855b0571b411e40a0ab3f82b7d52;hpb=99ca90bf28a25fcd1cd84596c37be43c97f74e6e;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/formal_topology2.ma b/helm/software/matita/contribs/formal_topology/formal_topology2.ma
index b98865a5c..10666ba35 100644
--- a/helm/software/matita/contribs/formal_topology/formal_topology2.ma
+++ b/helm/software/matita/contribs/formal_topology/formal_topology2.ma
@@ -27,8 +27,7 @@ axiom one: S.
 notation "1" with precedence 89
 for @{ 'unit }.
 
-interpretation "Unit" 'unit =
- cic:/matita/formal_topology/one.con.
+interpretation "Unit" 'unit = one.
  
 axiom one_left: ∀A. 1 A = A.
 axiom one_right: ∀A:S. A 1 = A.
@@ -39,10 +38,7 @@ axiom eps_idempotent: eps = eps eps.
 notation "hvbox(A break ⊆ B)" with precedence 59
 for @{ 'subseteq $A $B}.
 
-interpretation "Subseteq" 'subseteq A B =
- (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ A
-  (cic:/matita/formal_topology/comp.con
-   cic:/matita/formal_topology/eps.con B)).
+interpretation "Subseteq" 'subseteq A B = (eq _ A (comp eps B)).
 
 axiom leq_refl: ∀A. A ⊆ A.
 axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
@@ -74,4 +70,4 @@ theorem th4: ∀A. c A ⊆ (m (i (m A))). intros; auto. qed.
 theorem th5: ∀A. i (m A) = i (m (c A)). intros; auto. qed.
 theorem th6: ∀A. m (i A) = c (m (i A)). intros; auto. qed.
 
-theorem th7: ∀A. i (m (i A)) = i (s (i A)).
\ No newline at end of file
+theorem th7: ∀A. i (m (i A)) = i (s (i A)).