From: Enrico Tassi Date: Thu, 15 Jan 2009 15:36:52 +0000 (+0000) Subject: added notation for 'Vdash X-Git-Tag: make_still_working~4253 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bdd7585617c6977ce3dc0a84afb686d089435870;p=helm.git added notation for 'Vdash --- diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 9970c9cfb..8709f0265 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -225,3 +225,10 @@ notation "\integers" non associative with precedence 90 for @{'Z}. notation "\complexes" non associative with precedence 90 for @{'C}. notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *) + +notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}. +notation > "x ⊩_term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}. +notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}. +notation > "⊩ " with precedence 60 for @{'Vdash ?}. +notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}. +