From 2a3865b61ac21e3a5eabdef235339ee022b2c942 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 15 Oct 2007 11:38:14 +0000 Subject: [PATCH] The behaviour of autobatch paramodulation has changed. But autobatch works! Is the test still correct? --- matita/tests/naiveparamod.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/matita/tests/naiveparamod.ma b/matita/tests/naiveparamod.ma index 8b83331a2..624604842 100644 --- a/matita/tests/naiveparamod.ma +++ b/matita/tests/naiveparamod.ma @@ -30,7 +30,7 @@ theorem prova1: C. intros (A B C S a w h b wb). (* exact (h s (a b) b wb II). *) - autobatch new width = 5 depth = 3. (* look at h parameters! *) + autobatch width = 5 depth = 3. (* look at h parameters! *) qed. (* c'e' qualcosa di imperativo, se si cambia l'rdine delle ipotesi poi sclera *) @@ -44,4 +44,4 @@ theorem prova2: intros. autobatch paramodulation. try assumption. - qed. + qed. \ No newline at end of file -- 2.39.2