From 41a2cd9f8efb97c0e89c65adbd46d0ff751d2e6c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 11 Jul 2007 09:16:43 +0000
Subject: [PATCH] auto new => autobatch

---
 helm/software/matita/dama/reals.ma         | 2 +-
 helm/software/matita/dama/vector_spaces.ma | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

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 
   ].
diff --git a/helm/software/matita/dama/vector_spaces.ma b/helm/software/matita/dama/vector_spaces.ma
index de4af986a..6aaebd12b 100644
--- a/helm/software/matita/dama/vector_spaces.ma
+++ b/helm/software/matita/dama/vector_spaces.ma
@@ -127,7 +127,7 @@ apply
      d (f j) l ≤ inv R (sum_field ? (S n)) ?);
  apply not_eq_sum_field_zero;
  unfold;
- auto new.
+ autobatch.
 qed.
 
 definition is_cauchy_seq : ∀R:real.\forall V:vector_space R.
@@ -141,7 +141,7 @@ definition is_cauchy_seq : ∀R:real.\forall V:vector_space R.
       d (f N)  (f n)≤ inv R (sum_field R (S m)) ?);
  apply not_eq_sum_field_zero;
  unfold;
- auto.
+ autobatch.
 qed.
 
 definition is_complete ≝
-- 
2.39.2