X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fformal_topology.ma;h=63da5347726baff4f1ab833606f54cef6c89b3d8;hb=fc1e871dde0f9f4cfde6f4a4fda8d18022584e65;hp=8e957e8b64975bf8942be23ee6c3900097493e91;hpb=dcef667a444aa0f189225855c1433d26b65fb8b7;p=helm.git

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 8e957e8b6..63da53477 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -17,23 +17,23 @@ include "logic/cprop_connectives.ma".
 
 record powerset (A : Type) : Type ≝ { char : A → CProp }.
 
-interpretation "char" 'subset p = (mk_powerset _ p).  
+interpretation "char" 'subset p = (mk_powerset ? p).  
 
 interpretation "pwset" 'powerset a = (powerset a). 
 
-interpretation "in" 'mem a X = (char _ X a). 
+interpretation "in" 'mem a X = (char ? X a). 
 
 definition subseteq ≝ λA.λu,v:\Omega \sup A.∀x.x ∈ u → x ∈ v.
 
-interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
+interpretation "subseteq" 'subseteq u v = (subseteq ? u v).
 
 definition overlaps ≝ λA.λU,V : Ω \sup A. exT2 ? (λx.x ∈ U) (λx.x ∈ V).
 
-interpretation "overlaps" 'overlaps u v = (overlaps _ u v).
+interpretation "overlaps" 'overlaps u v = (overlaps ? u v).
 
 definition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
 
-interpretation "intersect" 'intersects u v = (intersect _ u v). 
+interpretation "intersect" 'intersects u v = (intersect ? u v). 
 
 record axiom_set : Type ≝ { 
   A:> Type;
@@ -51,8 +51,8 @@ inductive covers (A: axiom_set) (U: \Omega \sup A) : A → CProp ≝
 notation "hvbox(a break ◃ b)" non associative with precedence 45
 for @{ 'covers $a $b }. (* a \ltri b *)
 
-interpretation "coversl" 'covers A U = (for_all _ U A (covers _ U)).
-interpretation "covers" 'covers a U = (covers _ U a).
+interpretation "coversl" 'covers A U = (for_all ? U A (covers ? U)).
+interpretation "covers" 'covers a U = (covers ? U a).
 
 definition covers_elim ≝
  λA:axiom_set.λU: \Omega \sup A.λP:\Omega \sup A.
@@ -77,8 +77,8 @@ coinductive fish (A:axiom_set) (U: \Omega \sup A) : A → CProp ≝
 notation "hvbox(a break ⋉ b)" non associative with precedence 45
 for @{ 'fish $a $b }. (* a \ltimes b *)
 
-interpretation "fishl" 'fish A U = (ex_such _ U A (fish _ U)).
-interpretation "fish" 'fish a U = (fish _ U a).
+interpretation "fishl" 'fish A U = (ex_such ? U A (fish ? U)).
+interpretation "fish" 'fish a U = (fish ? U a).
 
 let corec fish_rec (A:axiom_set) (U: \Omega \sup A)
  (P: Ω \sup A) (H1: P ⊆ U)
@@ -154,7 +154,7 @@ qed.
 
 definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
 
-interpretation "covered by one" 'leq a b = (leq _ a b).
+interpretation "covered by one" 'leq a b = (leq ? a b).
 
 theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
  intros;
@@ -176,15 +176,15 @@ qed.
 
 definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
 
-interpretation "uparrow" 'uparrow a = (uparrow _ a).
+interpretation "uparrow" 'uparrow a = (uparrow ? a).
 
 definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
 
-interpretation "downarrow" 'downarrow a = (downarrow _ a).
+interpretation "downarrow" 'downarrow a = (downarrow ? a).
 
 definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
 
-interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
 
 record convergent_generated_topology : Type ≝
  { AA:> axiom_set;