interpretation for <->

diff --git a/helm/software/matita/nlibrary/Plogic/connectives.ma b/helm/software/matita/nlibrary/Plogic/connectives.ma
index 491657676a85ada0ae073947190306fedbb0af87..bf17771fb9890a632f0f49f2b8e223837712f36a 100644 (file)
--- 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).