auto calls cleanup\

[helm.git] / helm / software / matita / library / nat / factorization.ma

diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma
index 1ca684aed0692c05874db9dd9c1a5ca0174d3739..f17fe03080e1e7b793e72cce687064449f811f40 100644 (file)
--- 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.