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

---
 helm/software/matita/dama/ordered_fields_ch0.ma | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma
index 191137933..d423894d0 100644
--- a/helm/software/matita/dama/ordered_fields_ch0.ma
+++ b/helm/software/matita/dama/ordered_fields_ch0.ma
@@ -120,7 +120,7 @@ definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
      f j ≤ l + (inv F (sum_field ? (S n)) ?));
  apply not_eq_sum_field_zero;
  unfold;
- auto new.
+ autobatch.
 qed.
 
 (*
@@ -142,7 +142,7 @@ definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
       f N - f n ≤ inv ? (sum_field F (S m)) ?);
  apply not_eq_sum_field_zero;
  unfold;
- auto.
+ autobatch.
 qed.
 
 definition is_complete ≝
-- 
2.39.2