From f3ad825f16c02c0c5fca620980882e409871e6f1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi <enrico.tassi@inria.fr> Date: Mon, 16 Jun 2008 12:42:38 +0000 Subject: [PATCH] typo --- helm/software/matita/contribs/dama/dama/supremum.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index 468c1d506..6d5879a83 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -216,7 +216,7 @@ qed. (* Definition 2.7 *) definition order_converge â λO:ordered_set.λa:sequence O.λx:O. - ExT23 (sequence O) (λl.l â x) (λu.u â x) + exT23 (sequence O) (λl.l â x) (λu.u â x) (λl,u.âi:nat. (l i) is_infimum âw,a (w+i)â ⧠(u i) is_supremum âw,a (w+i)â). -- 2.39.2