[mizar] adjectives vs Element of

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Dear All,

I am writing this email, which is addressed to all potential authors of new 
Mizar articles, on behalf of Library Committee.

You are kindly requested to use types like 'natural number' instead of 'Element 
of NAT', 'real number' instead of 'Element of REAL', 'complex number' instead 
of 'Element of COMPLEX', etc. Especially, please do not use 'Element of' in 
exportable part of articles. Only strongly needed usage of 'Element of' will be 
accepted by reviewers, who are just asked to pay particular attention to catch 
up all such cases.

The reason is that from technical point of view, for example, 'natural number' 
and 'Element of NAT' are not the same, even if they contain the same elements, 
since Mizar supports some automatizations to treat adjectives, which are not 
implemented for 'Element of'.

Thank you very much for your cooperation, in advance.

Best regards
Artur K