X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ffactorization.ma;h=f17fe03080e1e7b793e72cce687064449f811f40;hb=6719c0e318b312b51b089fea3d69d1b7103245ea;hp=1ca684aed0692c05874db9dd9c1a5ca0174d3739;hpb=c445ba5534cccde19016c92660ab52777af221c0;p=helm.git

diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma
index 1ca684aed..f17fe0308 100644
--- a/helm/software/matita/library/nat/factorization.ma
+++ b/helm/software/matita/library/nat/factorization.ma
@@ -61,7 +61,7 @@ cut (\exists i. nth_prime i = smallest_factor n);
       [ apply (trans_lt ? (S O));
         [ unfold lt; apply le_n;
         | apply lt_SO_smallest_factor; assumption; ]
-      | letin x \def le.autobatch new.
+      | letin x \def le.autobatch.
          (*       
        apply divides_smallest_factor_n;
         apply (trans_lt ? (S O));
@@ -144,7 +144,7 @@ apply divides_max_prime_factor_n.
 assumption.unfold Not.
 intro.
 cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
-  [unfold Not in Hcut1.autobatch new.
+  [unfold Not in Hcut1.autobatch.
     (*
     apply Hcut1.apply divides_to_mod_O;
     [ apply lt_O_nth_prime_n.