X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fordered_fields_ch0.ma;h=d423894d064b77a202ade901fdaca33c765a9c91;hb=dfc523454502ccab6a154a32d1d9b4d941d9a6a0;hp=1911379333608b2fdb1d28f80f40fd0b27ca5db2;hpb=06a089726af079d5b2fe42ba78632565dad0eb3e;p=helm.git

diff --git a/matita/dama/ordered_fields_ch0.ma b/matita/dama/ordered_fields_ch0.ma
index 191137933..d423894d0 100644
--- a/matita/dama/ordered_fields_ch0.ma
+++ b/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 ≝