X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fordered_sets.ma;h=62b9348659674a35114f6213157f2c20573ad552;hb=4a3ced7cc547cc4f4566c4c68c35b0de1aabf7f0;hp=1ca191339b697514c39b171ed9111ef8c6a1003c;hpb=c0e7999b2d7cb926affcf406f33e01e74bea62d7;p=helm.git

diff --git a/matita/dama/ordered_sets.ma b/matita/dama/ordered_sets.ma
index 1ca191339..62b934865 100644
--- a/matita/dama/ordered_sets.ma
+++ b/matita/dama/ordered_sets.ma
@@ -330,7 +330,7 @@ theorem tail_inf_increasing:
       assumption
     | unfold y;
       simplify;
-      auto paramodulation library
+      autobatch paramodulation library
     ]
  ].
 qed.