X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Ftests%2Ffguidi.ma;h=165f9ce302fd35e0c2aaa9776bfe652f3996484b;hb=91387f570cb178315c0f492e66e95c1efe5bab2c;hp=b1c17185d08dfabb33aff29c2576307ad7cb59fb;hpb=b70dd6eca72985b11d7d223b8a6a84fda44cdf69;p=helm.git

diff --git a/matita/tests/fguidi.ma b/matita/tests/fguidi.ma
index b1c17185d..165f9ce30 100644
--- a/matita/tests/fguidi.ma
+++ b/matita/tests/fguidi.ma
@@ -84,8 +84,8 @@ theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to
 intros 4. elim H; clear H x y.
 apply eq_gen_S_O. exact m. elim H1. auto paramodulation.
 clear H2. cut (n = m).
-elim Hcut. apply ex_intro. exact n1. split; auto.
-apply eq_gen_S_S. auto.
+elim Hcut. apply ex_intro. exact n1. split; autobatch.
+apply eq_gen_S_S. autobatch.
 qed.
 
 theorem le_gen_S_x: \forall m,x. (le (S m) x) \to 
@@ -113,5 +113,5 @@ qed.
 theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
 intros 1. elim x; clear H. clear x. 
 auto paramodulation.
-fwd H1 [H]. decompose H.
+fwd H1 [H]. decompose.
 *)