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