auto calls cleanup\

diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
index 8613d83e2ba486c110c817fed6107ef41c33179b..1ce9f1f9be395772a5054ef09b86af03e0c5421d 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
+++ b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
@@ -136,7 +136,7 @@ intros (H2 H3).
 elim (H1 e) 0.
 clear H1.
 intros (H4 H5).
-autobatch new.
+autobatch.
 qed.
 (*
 astepr (e[+]f). 

diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
index 9fb4073bac8730da01aa0b78d5745f590ade3e38..ad16edf7bf6c5f6fc6611e184ac6ab1814e30b32 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
+++ b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
@@ -473,7 +473,7 @@ simplify.
 right. apply I|intros (a at).simplify. left. apply I]]
 simplify.
 left.
-autobatch new|intros 2 (c l).
+autobatch |intros 2 (c l).
 intros 2 (Hy).
 elim y 0[
 intros 2 (H z).
@@ -509,15 +509,15 @@ unfold Not.
 elim x 0[
   intro y.
   elim y 0[
-    split[simplify.intro.autobatch new|simplify.intros.exact H1]|
+    split[simplify.intro.autobatch|simplify.intros.exact H1]|
 intros (a at).
 simplify.
-split[intro.autobatch new|intros. exact H1]
+split[intro.autobatch|intros. exact H1]
 ]
 |
 intros (a at IHx).
 elim y 0[simplify.
-  split[intro.autobatch new|intros.exact H]
+  split[intro.autobatch|intros.exact H]
   |
 intros 2 (c l).
 generalize in match (IHx l).

diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma
index 3b37dc42b069e329270626d8f624e9b3f8d59249..ee5f99610ed7be4c91f32c4835c4ed61ef3e3cbd 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/Setoids.ma
+++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma
@@ -1263,7 +1263,7 @@ apply f. apply n1. apply m1.
 apply eq_symmetric_unfolded.assumption.
 apply eq_symmetric_unfolded.assumption.
 apply H.
-autobatch new.
+autobatch.
 qed.
 
 (*

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.