The order of articles in the NotationDirective? is important. If two definitions of the same symbol from two different articles mentioned in notation are applicable in your article, the definition from the latter article is used.

Moreover, Mizar does not use context to decide between the variants. So even if it is clear (to you) from the type declaration of the superterm functor (or predicate or other constructor), which variant should be used to make the superterm parsable, Mizar will still require to have the articles in the NotationDirective? in proper order.

-- JosefUrban - 12 Jul 2002