auto calls cleanup\

[helm.git] / helm / software / matita / library / algebra / CoRN / SetoidFun.ma

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).