removed no longer used METAs

[helm.git] / helm / matita / contribs / PREDICATIVE-TOPOLOGY / iff.ma

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma
index e6475c5fdafcadb59a37891950c839e6a9e6e0a2..9a9491923f889afb28808116a23eb121fa77473c 100644 (file)
--- 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 }.