From bdd7585617c6977ce3dc0a84afb686d089435870 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Jan 2009 15:36:52 +0000 Subject: [PATCH] added notation for 'Vdash --- helm/software/matita/core_notation.moo | 7 +++++++ 1 file changed, 7 insertions(+) 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}. + -- 2.39.2