]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/algebra/CoRN/Setoids.ma
auto calls cleanup\
[helm.git] / helm / software / matita / library / algebra / CoRN / Setoids.ma
index 3b37dc42b069e329270626d8f624e9b3f8d59249..ee5f99610ed7be4c91f32c4835c4ed61ef3e3cbd 100644 (file)
@@ -1263,7 +1263,7 @@ apply f. apply n1. apply m1.
 apply eq_symmetric_unfolded.assumption.
 apply eq_symmetric_unfolded.assumption.
 apply H.
-autobatch new.
+autobatch.
 qed.
 
 (*