X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsupremum.ma;h=f53cdc45814862a707493c7b3409a84bf7d75377;hb=25aa80d913c903fcc270d05464cf3084b12d52a8;hp=6d5879a8378e6fcd92c71dfeeba7785af5942580;hpb=6d4c63a0ff7d44e4e361fc4aeca8028a77d39568;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 6d5879a83..f53cdc458 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -220,7 +220,7 @@ definition order_converge ≝
      (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
                    (u i) is_supremum ⌊w,a (w+i)⌋).
     
-notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
+notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
   for @{'order_converge $a $x}.
 notation > "a 'order_converges' x" non associative with precedence 45 
   for @{'order_converge $a $x}.