From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 27 May 2008 08:36:21 +0000 (+0000)
Subject: auto calls cleanup\
X-Git-Tag: make_still_working~5124
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7f664e6b4cda35865cb3619800527204a651ba3;p=helm.git

auto calls cleanup\
---

diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
index 8613d83e2..1ce9f1f9b 100644
--- 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 9fb4073ba..ad16edf7b 100644
--- 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 3b37dc42b..ee5f99610 100644
--- 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 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.