- new notation.ma file with local and common notation

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / basic_pairs.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
index 6140e278ec5c30e0d8624d90c0b50624f67ccde9..84f48c894282c7a1971ed4f52c63d9ab6f0a0a20 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "relations.ma".
+include "notation.ma".
 
 record basic_pair: Type1 ≝
  { concr: REL;
@@ -31,8 +32,6 @@ record relation_pair (BP1,BP2: basic_pair): Type1 ≝
    commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩
  }.
 
-notation "hvbox (r \sub \c)"  with precedence 90 for @{'concr_rel $r}.
-notation "hvbox (r \sub \f)"  with precedence 90 for @{'form_rel $r}.
 
 interpretation "concrete relation" 'concr_rel r = (concr_rel __ r). 
 interpretation "formal relation" 'form_rel r = (form_rel __ r).