From: Enrico Tassi Date: Sun, 28 Dec 2008 18:06:59 +0000 (+0000) Subject: removed duplicate notation X-Git-Tag: make_still_working~4311 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2834b00a47f54b1fcc027ffe00f05600e735358;p=helm.git removed duplicate notation --- diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 3e03cb093..6b91c99b8 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -393,6 +393,5 @@ qed. coercion hint. interpretation "SET dagger" 'prop1 h = (prop11_SET1 _ _ _ _ _ h). -notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }. interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b). interpretation "SET1 eq" 'eq x y = (eq_rel1 _ (eq'' _) x y).