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

diff --git a/helm/software/matita/library/nat/euler_theorem.ma b/helm/software/matita/library/nat/euler_theorem.ma
index 43638fca6..d45c15dc3 100644
--- a/helm/software/matita/library/nat/euler_theorem.ma
+++ b/helm/software/matita/library/nat/euler_theorem.ma
@@ -77,8 +77,8 @@ intros 3.elim H
   [rewrite > pi_p_S.
    cut (eqb (gcd (S O) n) (S O) = true)
     [rewrite > Hcut.
-     change with ((gcd n (S O)) = (S O)).auto
-    |apply eq_to_eqb_true.auto
+     change with ((gcd n (S O)) = (S O)).autobatch
+    |apply eq_to_eqb_true.autobatch
     ]
   |rewrite > pi_p_S.
    apply eqb_elim
@@ -189,11 +189,11 @@ split
             |apply mod_O_to_divides
               [assumption
               |rewrite > distr_times_minus.
-               auto
+               autobatch
               ]
             ]
           ]
-        |auto
+        |autobatch
         ]
       ]
     |intro.assumption
@@ -214,11 +214,11 @@ split
             |apply mod_O_to_divides
               [assumption
               |rewrite > distr_times_minus.
-               auto
+               autobatch
               ]
             ]
           ]
-        |auto
+        |autobatch
         ]
       ]
     ]