auto => autobatch

[helm.git] / matita / tests / inversion.ma

diff --git a/matita/tests/inversion.ma b/matita/tests/inversion.ma
index 07d3a0c4a09f9e90ef82a7048559b473f4517fd7..4c33beee0f8c38a89b79f366c4e573e378881c90 100644 (file)
--- a/matita/tests/inversion.ma
+++ b/matita/tests/inversion.ma
@@ -42,7 +42,7 @@ theorem t: \forall x,y. \forall H: sum x y O.
  simplify. intros.
  generalize in match H1.
  rewrite < H2; rewrite < H3.intro.
- rewrite > H4.auto new library.
+ rewrite > H4.autobatch library.
 qed.
 
 theorem t1: \forall x,y. sum x y O \to x = y.
@@ -57,5 +57,5 @@ apply (sum_ind ? (\lambda a,b,K. y=a \to O=b \to x=a) ? ? ? s).*)
 inversion s.
 intros.simplify.
 intros.
-rewrite > H. rewrite < H2.  auto new library.
+rewrite > H. rewrite < H2.  autobatch library.
 qed.