From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 16 Sep 2005 12:13:31 +0000 (+0000)
Subject: added notation for: nleq, ngeq, nless, and ngtr
X-Git-Tag: LAST_BEFORE_NEW~114
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3dae7afc87ba1c04906bd4268e2c5a9e98f72361;p=helm.git

added notation for: nleq, ngeq, nless, and ngtr
---

diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo
index 38c1a4efa..c528fc111 100644
--- a/helm/matita/core_notation.moo
+++ b/helm/matita/core_notation.moo
@@ -30,6 +30,22 @@ notation "hvbox(a break \neq b)"
   non associative with precedence 45
 for @{ 'neq $a $b }.
 
+notation "hvbox(a break \nleq b)" 
+  non associative with precedence 45
+for @{ 'nleq $a $b }.
+
+notation "hvbox(a break \ngeq b)" 
+  non associative with precedence 45
+for @{ 'ngeq $a $b }.
+
+notation "hvbox(a break \nless b)" 
+  non associative with precedence 45
+for @{ 'nless $a $b }.
+
+notation "hvbox(a break \ngtr b)" 
+  non associative with precedence 45
+for @{ 'ngtr $a $b }.
+
 notation "hvbox(a break + b)" 
   left associative with precedence 50
 for @{ 'plus $a $b }.