X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Freals.ma;h=d57e6cfba62f8cada56b0da615a5b07fa5df3d12;hb=c4050b216986232e7ad0095542b940960626614b;hp=87bbee5fd0d2e84de0a9e49d8ee066f4d826e8b8;hpb=d8d87f227a8abb5cb324c6e8c6bf66ee83ead553;p=helm.git

diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma
index 87bbee5fd..d57e6cfba 100644
--- a/helm/software/matita/dama/reals.ma
+++ b/helm/software/matita/dama/reals.ma
@@ -39,7 +39,7 @@ definition max_seq: ∀R:real.∀x,y:R. nat → R.
   [ apply x
   | apply not_eq_sum_field_zero ;
     unfold;
-    auto new
+    autobatch
   | apply y
   | apply lt_zero_to_le_inv_zero 
   ].