A very nice experiment using notation: we define the notation for natural

[helm.git] / helm / software / matita / library / logic / coimplication.ma

diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma
index 9edb4949c532c23ee43679ae11ad2ecac123d4bf..a8fc4a232fbbcfc3eadca0a4476632f10bce23da 100644 (file)
--- a/helm/software/matita/library/logic/coimplication.ma
+++ b/helm/software/matita/library/logic/coimplication.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/logic/coimplication".
-
 include "logic/connectives.ma".
 
 definition Iff : Prop \to Prop \to Prop \def
@@ -31,17 +29,17 @@ 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.
- intros. decompose. apply iff_intro; intros; auto.
+ intros. elim H. apply iff_intro[assumption|assumption]
 qed.
 
 theorem iff_trans: \forall A,B,C. A \liff B \to B \liff C \to A \liff C.
- intros. decompose. apply iff_intro; intros; auto.
+ intros. elim H. elim H1. apply iff_intro;intros;autobatch.
 qed.