X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fformal_topology.ma;h=15da20a1132aae02cb7df0a5b457096402649eb2;hb=01001c883a8151edba81cd03a6f254d24a81c867;hp=190e00e5d0eb549e6822d06c0e72fc6d9efe18a4;hpb=7a29aa43eb607d019699f0a76dc83e7093e5b222;p=helm.git

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 190e00e5d..15da20a11 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -158,13 +158,9 @@ qed.
 
 definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
 
-notation "↑a" with precedence 80 for @{ 'uparrow $a }.
-
 interpretation "uparrow" 'uparrow a = (uparrow _ a).
 
-definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
-
-notation "↓a" with precedence 80 for @{ 'downarrow $a }.
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
 
 interpretation "downarrow" 'downarrow a = (downarrow _ a).
 
@@ -172,9 +168,7 @@ definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
 
 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 
-(*
 record convergent_generated_topology : Type ≝
  { AA:> axiom_set;
    convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
  }.
-*)