From a3acd934eba07f24937e59c3c7a41db82d901025 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 14:25:17 +0000 Subject: [PATCH] Text fixed (due to stricter semantics for naming the binders in the patterns). --- helm/matita/tests/rewrite.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index ce1e216ad..bf4f3a6e5 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -14,7 +14,7 @@ rewrite < H in \vdash (? ? ? ((\lambda j.((\lambda w.%) ?)) ?)). rewrite < H in \vdash (? ? % ?). -simplify in \vdash (? ? ? ((\lambda x.((\lambda y.%) ?)) ?)). +simplify in \vdash (? ? ? ((\lambda _.((\lambda _.%) ?)) ?)). rewrite < H in \vdash (? ? ? (% ?)). simplify. -- 2.39.2