X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fmatita%2Fcontribs%2FPREDICATIVE-TOPOLOGY%2Fiff.ma;h=9a9491923f889afb28808116a23eb121fa77473c;hb=f104e539b06bf5695f4d526d5217a581f5a9c5f5;hp=e6475c5fdafcadb59a37891950c839e6a9e6e0a2;hpb=b2b7dd94197364a06841a8ef178e94fe7bfac57b;p=helm.git

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
index e6475c5fd..9a9491923 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
@@ -14,12 +14,18 @@
 
 set "baseuri" "cic:/matita/logic/iff".
 
+include "../../library/logic/connectives.ma".
+
 definition Iff : Prop \to Prop \to Prop \def
    \lambda A,B. (A \to B) \land (B \to A).
    
  (*CSC: the URI must disappear: there is a bug now *)
 interpretation "logical iff" 'iff x y = (cic:/matita/logic/iff/Iff.con x y).
 
-notation < "hvbox(a break \liff b)" 
+notation > "hvbox(a break \liff b)" 
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation < "hvbox(a break \leftrightarrow b)" 
   left associative with precedence 25
 for @{ 'iff $a $b }.