more push/pop to avoid confusion with imperative data structures employed by

[helm.git] / helm / software / matita / library / demo / formal_topology.ma

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 190e00e5d0eb549e6822d06c0e72fc6d9efe18a4..15da20a1132aae02cb7df0a5b457096402649eb2 100644 (file)
--- 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)
  }.
-*)