From d86eefac7dff521eb2589b6f2dcb8a1b361be186 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 23 Sep 2010 22:36:07 +0000
Subject: [PATCH] interpretation for <->

---
 helm/software/matita/nlibrary/Plogic/connectives.ma | 2 ++
 1 file changed, 2 insertions(+)

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).  
-- 
2.39.2