From 67906d4803b6bb6740382d8cbd31d8c0e7322c7d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 13 Sep 2005 12:12:44 +0000 Subject: [PATCH] Test fixed. --- helm/matita/tests/generalize.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/tests/generalize.ma b/helm/matita/tests/generalize.ma index ee0732225..aca28ffdc 100644 --- a/helm/matita/tests/generalize.ma +++ b/helm/matita/tests/generalize.ma @@ -31,7 +31,7 @@ qed. (* This test used to fail because x was used in the wrong context *) (* Once this was fixed it still did not work since apply is not *) (* able to solve a goal that ends in a product. *) -theorem test2: \forall x. x + 4 = 4 + x. +theorem test2: \forall x. 4 + x = x + 4. generalize in match 4. exact plus_comm. qed. -- 2.39.2