X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fnotation.ma;h=2cb92807d142ec9804e4eb98d8134c3a266e1012;hb=ccac4e720ff2a9bee8e1c9d5ba1ea6474db72572;hp=97c1a9b6dfb67c738f0ed3addc7a8d0f30171ba0;hpb=13114a0147a28f8c7359c9c19ee254716eb5f55a;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/notation.ma b/helm/software/matita/contribs/formal_topology/overlap/notation.ma
index 97c1a9b6d..2cb92807d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/notation.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/notation.ma
@@ -14,3 +14,10 @@
 
 notation "hvbox (r \sub \c)"  with precedence 90 for @{'concr_rel $r}.
 notation "hvbox (r \sub \f)"  with precedence 90 for @{'form_rel $r}.
+
+notation < "mstyle color #ff0000 (…)" non associative with precedence 90
+for @{'hide}.
+
+definition hide ≝ λA:Type.λx:A.x.
+
+interpretation "hide" 'hide = (hide _ _).