X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flogic%2Fcoimplication.ma;h=a963846f093a1cc362447baa2e85011539f5998d;hb=bccbeb1ec0ef3b55625e4434e693db3cce2e69be;hp=24965d72ce063f6209259812b1b189b661a5f331;hpb=c63590f609ffda64f0af782bccb127e1701c34d7;p=helm.git

diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma
index 24965d72c..a963846f0 100644
--- a/helm/software/matita/library/logic/coimplication.ma
+++ b/helm/software/matita/library/logic/coimplication.ma
@@ -31,11 +31,11 @@ notation < "hvbox(a break \leftrightarrow b)"
 for @{ 'iff $a $b }.
 
 theorem iff_intro: \forall A,B. (A \to B) \to (B \to A) \to (A \liff B).
- unfold Iff. intros. split; intros; auto.
+ unfold Iff. intros. split; intros; autobatch.
 qed.
 
 theorem iff_refl: \forall A. A \liff A.
- intros. apply iff_intro; intros; auto.
+ intros. apply iff_intro; intros; autobatch.
 qed.
 
 theorem iff_sym: \forall A,B. A \liff B \to B \liff A.
@@ -43,5 +43,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;auto.
+ intros. elim H. elim H1. apply iff_intro;intros;autobatch.
 qed.