From b1129a0a78ebf49c029420216fe94e16f8b0b76b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 26 Jul 2006 09:17:25 +0000 Subject: [PATCH] added test for reordering of goals when using the 1,2,3: tinycal --- matita/tests/tinycals.ma | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/matita/tests/tinycals.ma b/matita/tests/tinycals.ma index 7bc189261..960051672 100644 --- a/matita/tests/tinycals.ma +++ b/matita/tests/tinycals.ma @@ -15,12 +15,14 @@ set "baseuri" "cic:/matita/test/tinycals". theorem prova: - \forall A,B:Prop. - \forall H:A \to A \to A \to A \to A \to B.A \to B. + \forall A,B,C:Prop. + \forall H:A \to A \to C \to A \to A \to B.A \to C \to B. intros. apply H; [assumption - |3,5:assumption; + |3,5: + [ exact H2; + | exact H1 ] |4:assumption |*:assumption ] -- 2.39.2