X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fdiv_and_mod_new.ma;h=2f881b1551a564fb32107ec4c7bcf5f48d07c691;hb=a180bddcd4a8f35de3d7292162ba05d0077723aa;hp=325244f7a4708fbd3777530ed972c916721ab386;hpb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;p=helm.git

diff --git a/helm/software/matita/library/nat/div_and_mod_new.ma b/helm/software/matita/library/nat/div_and_mod_new.ma
index 325244f7a..2f881b155 100644
--- a/helm/software/matita/library/nat/div_and_mod_new.ma
+++ b/helm/software/matita/library/nat/div_and_mod_new.ma
@@ -151,7 +151,7 @@ qed.
 
 theorem div_mod_spec_div_mod: 
 \forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
-intros.auto.
+intros.autobatch.
 (*
 apply div_mod_spec_intro.
 apply lt_mod_m_m.assumption.
@@ -170,7 +170,7 @@ apply (nat_compare_elim q q1);intro
         [apply (lt_to_not_le r b H2 Hcut2)
         |elim Hcut.assumption
         ]
-      |auto depth=4. apply (trans_le ? ((q1-q)*b))
+      |autobatch depth=4. apply (trans_le ? ((q1-q)*b))
         [apply le_times_n.
          apply le_SO_minus.exact H6
         |rewrite < sym_plus.
@@ -180,7 +180,7 @@ apply (nat_compare_elim q q1);intro
     |rewrite < sym_times.
      rewrite > distr_times_minus.
      rewrite > plus_minus
-      [auto.
+      [autobatch.
        (*
        rewrite > sym_times.
        rewrite < H5.
@@ -188,7 +188,7 @@ apply (nat_compare_elim q q1);intro
        apply plus_to_minus.
        apply H3
        *)
-      |auto.
+      |autobatch.
        (*
        apply le_times_r.
        apply lt_to_le.