X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flogic%2Fconnectives2.ma;h=bc577a5f46dfd2ed235d81d9dd45de9336674720;hb=3c4660604bb23d862c72f64e6b5b5974260eea28;hp=fcc29e81a55bfb122a95b95a39733c68629dea48;hpb=c48de1fba2742df0d3ab42d69e758ae2859316d0;p=helm.git

diff --git a/helm/software/matita/library/logic/connectives2.ma b/helm/software/matita/library/logic/connectives2.ma
index fcc29e81a..bc577a5f4 100644
--- a/helm/software/matita/library/logic/connectives2.ma
+++ b/helm/software/matita/library/logic/connectives2.ma
@@ -39,6 +39,6 @@ theorem transitive_iff: transitive ? iff.
  elim H1;
  split;
  intro;
- auto.
+ autobatch.
 qed.