more work, but russell too slow

[helm.git] / helm / software / matita / contribs / dama / dama / supremum.ma

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 6d5879a8378e6fcd92c71dfeeba7785af5942580..f53cdc45814862a707493c7b3409a84bf7d75377 100644 (file)
--- 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}.