X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2FCoRN%2FSetoidFun.ma;h=ad16edf7bf6c5f6fc6611e184ac6ab1814e30b32;hb=a7f664e6b4cda35865cb3619800527204a651ba3;hp=9fb4073bac8730da01aa0b78d5745f590ade3e38;hpb=f63e9358746f82de0dd07d60bdf82fdc0fae2101;p=helm.git

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