From 2dd8be781f939739e1410dce3706ccc19a990525 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 --- helm/software/matita/tests/tinycals.ma | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/tests/tinycals.ma b/helm/software/matita/tests/tinycals.ma index 7bc189261..960051672 100644 --- a/helm/software/matita/tests/tinycals.ma +++ b/helm/software/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