X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FRELATIONAL%2FZEq%2Fsetoid.ma;h=6721926b10281e551c51710c43ed67d5c66f490e;hb=871d9b1d66f79445e7afa6d42205aaf33576c4f0;hp=1b6279fd1c57064bafd1c5b953da58325cb1996d;hpb=43ed97bb09bf148dfda74b3266b44143640b9643;p=helm.git

diff --git a/matita/contribs/RELATIONAL/ZEq/setoid.ma b/matita/contribs/RELATIONAL/ZEq/setoid.ma
index 1b6279fd1..6721926b1 100644
--- a/matita/contribs/RELATIONAL/ZEq/setoid.ma
+++ b/matita/contribs/RELATIONAL/ZEq/setoid.ma
@@ -20,11 +20,11 @@ include "ZEq/defs.ma".
 theorem zeq_refl: \forall z. z = z.
  intros. elim z. clear z.
  lapply (nplus_total t t1). decompose.
- auto.
+ autobatch.
 qed.
 
 theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1.
- intros. elim H. clear H z1 z2. auto.
+ intros. elim H. clear H z1 z2. autobatch.
 qed.
 (*
 theorem zeq_trans: \forall z1,z2. z1 = z2 \to