some old auto yurned into autobatch

[helm.git] / matita / contribs / RELATIONAL / ZEq / setoid.ma

diff --git a/matita/contribs/RELATIONAL/ZEq/setoid.ma b/matita/contribs/RELATIONAL/ZEq/setoid.ma
index 1b6279fd1c57064bafd1c5b953da58325cb1996d..6721926b10281e551c51710c43ed67d5c66f490e 100644 (file)
--- 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