X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcore_notation.moo;fp=helm%2Fsoftware%2Fmatita%2Fcore_notation.moo;h=8709f0265161c69d0593177b7ab74cc65c9988f3;hb=bdd7585617c6977ce3dc0a84afb686d089435870;hp=9970c9cfb6d6d331dd4847490f399e6e197ca9fb;hpb=7f492f1ed0024596094fc6585c604fd814ea8b60;p=helm.git

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}.
+