From 136983c7fcee33144364468672a675a6275a7b9f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 17 Nov 2005 18:39:16 +0000 Subject: [PATCH 1/1] New test for parallel rewriting in the hypotheses and in the conclusion. --- helm/matita/tests/rewrite.ma | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index 194dbd17e..a69e33d77 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -48,9 +48,17 @@ theorem foo: \forall n. n = n + 0. rewrite < t; reflexivity. qed. -theorem test_rewrite_in_hyp: \forall n,m. n + 0 = m \to m = n + 0 \to n=m \land m+0=n+0. +theorem test_rewrite_in_hyp: + \forall n,m. n + 0 = m \to m = n + 0 \to n=m \land m+0=n+0. intros. rewrite < plus_n_O in H. rewrite > plus_n_O in H1. split; [ exact H | exact H1]. qed. + +theorem test_rewrite_in_hyp2: + \forall n,m. n + 0 = m \to n + 0 = m \to n=m \land n+0=m. + intros. + rewrite < plus_n_O in H H1 \vdash (? ? %). + split; [ exact H | exact H1]. +qed. -- 2.39.2