From 2528d5a1b74beb1ec4bebe4c34dcf557d57a9d86 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 12:22:36 +0000 Subject: [PATCH] ... --- helm/software/matita/tests/paramodulation/group.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/tests/paramodulation/group.ma b/helm/software/matita/tests/paramodulation/group.ma index fc2ff14ce..d4c6bf879 100644 --- a/helm/software/matita/tests/paramodulation/group.ma +++ b/helm/software/matita/tests/paramodulation/group.ma @@ -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. +intros.auto paramodulation;exact a. qed. -- 2.39.2