From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 23 Sep 2010 22:36:07 +0000 (+0000)
Subject: interpretation for <->
X-Git-Tag: make_still_working~2826
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d86eefac7dff521eb2589b6f2dcb8a1b361be186;p=helm.git

interpretation for <->
---

diff --git a/helm/software/matita/nlibrary/Plogic/connectives.ma b/helm/software/matita/nlibrary/Plogic/connectives.ma
index 491657676..bf17771fb 100644
--- a/helm/software/matita/nlibrary/Plogic/connectives.ma
+++ b/helm/software/matita/nlibrary/Plogic/connectives.ma
@@ -75,3 +75,5 @@ ninductive ex2 (A:Type[0]) (P,Q:A \to Prop) : Prop ≝
 
 ndefinition iff :=
  λ A,B. (A → B) ∧ (B → A).
+
+interpretation "iff" 'iff a b = (iff a b).