From da3c267935b503cd09fa878da669053b31ebcf0b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Jul 2007 09:16:43 +0000 Subject: [PATCH] auto new => autobatch --- matita/dama/reals.ma | 2 +- matita/dama/vector_spaces.ma | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/matita/dama/reals.ma b/matita/dama/reals.ma index 87bbee5fd..d57e6cfba 100644 --- a/matita/dama/reals.ma +++ b/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/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 ≝ -- 2.39.2