From: Ferruccio Guidi Date: Tue, 1 Jan 2019 13:30:18 +0000 (+0100) Subject: the decentralization of core notation continues ... X-Git-Tag: make_still_working~258 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bf816f05ddbe0ded4948dd33490619724dc4f7cf;p=helm.git the decentralization of core notation continues ... subseteq notation decentralized --- diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index a0ad502b9..3bf1de3b2 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -272,9 +272,6 @@ for @{ 'notmem $a $b }. notation "hvbox(a break ≬ b)" non associative with precedence 45 for @{ 'overlaps $a $b }. (* \between *) -notation "hvbox(a break ⊆ b)" non associative with precedence 45 -for @{ 'subseteq $a $b }. (* \subseteq *) - notation "hvbox(a break ∩ b)" left associative with precedence 60 for @{ 'intersects $a $b }. (* \cap *) diff --git a/matita/matita/lib/basics/core_notation/subseteq_2.ma b/matita/matita/lib/basics/core_notation/subseteq_2.ma new file mode 100644 index 000000000..bbfe6f527 --- /dev/null +++ b/matita/matita/lib/basics/core_notation/subseteq_2.ma @@ -0,0 +1,15 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +(* Core notation *******************************************************) + +notation "hvbox(a break ⊆ b)" non associative with precedence 45 +for @{ 'subseteq $a $b }. (* \subseteq *) diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index 24b2c9a9e..3133682db 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -11,6 +11,7 @@ include "basics/logic.ma". include "basics/core_notation/compose_2.ma". +include "basics/core_notation/subseteq_2.ma". (********** predicates *********) diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma index 2f570c18f..8e40b666b 100644 --- a/matita/matita/lib/basics/sets.ma +++ b/matita/matita/lib/basics/sets.ma @@ -11,6 +11,7 @@ include "basics/logic.ma". include "basics/core_notation/singl_1.ma". +include "basics/core_notation/subseteq_2.ma". (**** a subset of A is just an object of type A→Prop ****)