]> matita.cs.unibo.it Git - helm.git/commitdiff
auto->autobatch
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 9 Jul 2007 09:58:45 +0000 (09:58 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 9 Jul 2007 09:58:45 +0000 (09:58 +0000)
matita/tests/multiple_inheritance.ma

index 614f57ca9b219d37a64c80b31aed1ff5d8b6456d..413c42d443fbe83e0600cf5ed58fe3639f946363 100644 (file)
@@ -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