From af55e721b611647b5cb7d738441f10e5f1305747 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 17 Jun 2005 14:59:59 +0000 Subject: [PATCH] uses new pattern concrete syntax --- helm/matita/tests/rewrite.ma | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index 82f245185..56ea93bf8 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -4,8 +4,8 @@ alias symbol "eq" (instance 0) = "leibnitz's equality". alias symbol "plus" (instance 0) = "natural plus". theorem a: \forall a,b:nat. - a = b \to b + 0 = a. + a = b \to b + a = a + a. intros. -rewrite left H. -auto. +rewrite right H in (? ? % ?). +reflexivity. qed. \ No newline at end of file -- 2.39.2