[mizar] Question on Mizar grammar

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi all,

I have a question about Mizar grammar.

The Mizar article XBOOLE_0.miz contains the following fragment (which begins 
at line 160):

---------------------------------------------------
 redefine pred X = Y means
    X c= Y & Y c= X;
  compatibility
  proof
  .....
---------------------------------------------------

But the current rule for Predicate-Definition in syntax.txt states that:

---------------------------------------------------
Predicate-Definition =
   "pred" Predicate-Pattern [ "means" Definiens ] ";"
       [ "correctness" Justification ";" ] { Predicate-Property } .
---------------------------------------------------

There is no way to get terminal "compatibility" from this rule,
so something wrong with it.

Is it correct?

Michael Nedzelsky