From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 15 Sep 2005 09:38:00 +0000 (+0000)
Subject: added \neq notation
X-Git-Tag: LAST_BEFORE_NEW~125
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b86d8020e759afa1adcb8fe3571eeac288edfd83;p=helm.git

added \neq notation
---

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index a561827f8..84f7df2e6 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/logic/equality/".
 
 include "higher_order_defs/relations.ma".
+include "logic/connectives.ma".
 
 inductive eq (A:Type) (x:A) : A \to Prop \def
     refl_eq : eq A x x.
@@ -22,6 +23,10 @@ inductive eq (A:Type) (x:A) : A \to Prop \def
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "leibnitz's equality"
    'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "leibnitz's non-equality"
+  'neq x y = (cic:/matita/logic/connectives/Not.con
+    (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)).
 
 theorem reflexive_eq : \forall A:Type. reflexive A (eq A).
 simplify.intros.apply refl_eq.