X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flogic%2Fcoimplication.ma;h=44f8d5b8eb5f5f36f4affe1aefe4bb334ae6882b;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=a963846f093a1cc362447baa2e85011539f5998d;hpb=a180bddcd4a8f35de3d7292162ba05d0077723aa;p=helm.git

diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma
index a963846f0..44f8d5b8e 100644
--- a/helm/software/matita/library/logic/coimplication.ma
+++ b/helm/software/matita/library/logic/coimplication.ma
@@ -12,23 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/logic/coimplication".
-
 include "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/coimplication/Iff.con x y).
-
-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 }.
+interpretation "logical iff" 'iff x y = (Iff x y).
 
 theorem iff_intro: \forall A,B. (A \to B) \to (B \to A) \to (A \liff B).
  unfold Iff. intros. split; intros; autobatch.
@@ -43,5 +32,5 @@ theorem iff_sym: \forall A,B. A \liff B \to B \liff A.
 qed.
 
 theorem iff_trans: \forall A,B,C. A \liff B \to B \liff C \to A \liff C.
- intros. elim H. elim H1. apply iff_intro;intros;autobatch.
+ intros. elim H. elim H1. apply iff_intro;intros;autobatch depth=3.
 qed.