X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_sets.ma;h=62b9348659674a35114f6213157f2c20573ad552;hb=5e736134ceab076b4e963d535f380ffa796a5d19;hp=27b10aeefbac510bfc7d65a7d4ae70873a6483a0;hpb=603bbe202f09745133cefa4902f2b16fb17b70b8;p=helm.git

diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma
index 27b10aeef..62b934865 100644
--- a/helm/software/matita/dama/ordered_sets.ma
+++ b/helm/software/matita/dama/ordered_sets.ma
@@ -330,7 +330,7 @@ theorem tail_inf_increasing:
       assumption
     | unfold y;
       simplify;
-      auto paramodulation library
+      autobatch paramodulation library
     ]
  ].
 qed.
@@ -692,4 +692,4 @@ qed.
 definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b.
 
 interpretation "Ordered set lt" 'lt a b =
- (cic:/matita/ordered_sets/lt.con _ _ a b).
+ (cic:/matita/ordered_sets/lt.con _ a b).