X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Ftests%2Fmultiple_inheritance.ma;h=413c42d443fbe83e0600cf5ed58fe3639f946363;hb=630e4146e14848db27b89d1467c5120d46530bce;hp=614f57ca9b219d37a64c80b31aed1ff5d8b6456d;hpb=241dd3fc882e24a1d3a386a9c612aa8fc720abdb;p=helm.git diff --git a/matita/tests/multiple_inheritance.ma b/matita/tests/multiple_inheritance.ma index 614f57ca9..413c42d44 100644 --- a/matita/tests/multiple_inheritance.ma +++ b/matita/tests/multiple_inheritance.ma @@ -50,5 +50,5 @@ axiom mult_idempotent: ∀r2:R2.∀x:r2. mult ? x x = x. lemma test: ∀r:R. ∀x:r. f ? x = x. intros; unfold f; - auto paramodulation. + autobatch paramodulation. qed. \ No newline at end of file