Just a snapshot.

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-concrete_spaces.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
index e90ec7fe401942dc219b7d98be8669760cd9fabd..57ec577aec9d1248c0f70e521dc62329a4dafbeb 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
@@ -15,22 +15,6 @@
 include "o-basic_pairs.ma".
 include "o-saturations.ma".
 
-notation "□ \sub b" non associative with precedence 90 for @{'box $b}.
-notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}.
-interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (rel x)).
- 
-notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}.
-notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}.
-interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (rel x)).
-
-notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}.
-notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}.
-interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (rel x)).
-
-notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
-notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
-interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (rel x)).
-
 definition A : ∀b:BP. unary_morphism1 (form b) (form b).
 intros; constructor 1;
  [ apply (λx.□_b (Ext⎽b x));
@@ -161,4 +145,4 @@ definition CSPA: category2.
   | intros; simplify;
     change with (id2 ? o2 ∘ a = a);
     apply (id_neutral_left2 : ?);]
-qed.
\ No newline at end of file
+qed.