X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fvector_spaces.ma;h=6aaebd12bde8b9007229f21b9755b160d63df765;hb=5a8b5510d0b2d6dd1086658f97ce4f2186eced22;hp=de4af986a7a98d437ecf2ed3e6d46892a1304396;hpb=ac783aa7646c36a2c6db08ac8f21f1ec99cd55ee;p=helm.git

diff --git a/matita/dama/vector_spaces.ma b/matita/dama/vector_spaces.ma
index de4af986a..6aaebd12b 100644
--- a/matita/dama/vector_spaces.ma
+++ b/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 ≝