From c497867b0452f544661fd73b7f5dc8afbe8460e4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Jul 2007 13:46:07 +0000 Subject: [PATCH] auto -> autobatch --- helm/software/matita/tests/paramodulation/BOO075-1.ma | 2 +- .../software/matita/tests/paramodulation/boolean_algebra.ma | 2 +- helm/software/matita/tests/paramodulation/group.ma | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/tests/paramodulation/BOO075-1.ma b/helm/software/matita/tests/paramodulation/BOO075-1.ma index f266b1a94..7c46167f4 100644 --- a/helm/software/matita/tests/paramodulation/BOO075-1.ma +++ b/helm/software/matita/tests/paramodulation/BOO075-1.ma @@ -94,7 +94,7 @@ theorem prove_meredith_2_basis_1: \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (nand (nand A (nand (nand B A) A)) (nand B (nand C A))) B.eq Univ (nand (nand a a) (nand b a)) a . intros. -auto paramodulation timeout=600. +autobatch paramodulation timeout=600; try assumption. print proofterm. qed. diff --git a/helm/software/matita/tests/paramodulation/boolean_algebra.ma b/helm/software/matita/tests/paramodulation/boolean_algebra.ma index 85525db0e..ab47854da 100644 --- a/helm/software/matita/tests/paramodulation/boolean_algebra.ma +++ b/helm/software/matita/tests/paramodulation/boolean_algebra.ma @@ -516,5 +516,5 @@ theorem bool5: intros. unfold bool_algebra in H. decompose. -auto paramodulation. +autobatch paramodulation timeout=120. qed. diff --git a/helm/software/matita/tests/paramodulation/group.ma b/helm/software/matita/tests/paramodulation/group.ma index a19884d05..45fb3ad3d 100644 --- a/helm/software/matita/tests/paramodulation/group.ma +++ b/helm/software/matita/tests/paramodulation/group.ma @@ -29,7 +29,7 @@ theorem self: \forall H:(\forall x,y:A. x = y). \forall H:(\forall x,y,z:A. f x = y). \forall x,y:A. x=y. -intros.auto paramodulation. +intros.autobatch paramodulation. qed. theorem GRP049_simple: @@ -38,7 +38,7 @@ theorem GRP049_simple: \forall mult: A \to A \to A. \forall H: (\forall x,y,z:A.mult z (inv (mult (inv (mult (inv (mult z y)) x)) (inv (mult y (mult (inv y) y))))) = x). \forall a,b:A. mult (inv a) a = mult (inv b) b. -intros.auto paramodulation; +intros.autobatch paramodulation; qed. theorem GRP049 : @@ -47,5 +47,5 @@ theorem GRP049 : \forall mult: A \to A \to A. \forall H: (\forall x,y,z:A.mult z (inv (mult (inv (mult (inv (mult z y)) x)) (inv (mult y (mult (inv y) y))))) = x). \forall a,b:A. mult a (inv a)= mult b (inv b). -intros.auto paramodulation timeout = 600;exact a. +intros.autobatch paramodulation timeout = 600;exact a. qed. -- 2.39.2