[mizar] Mizar style, a story

[trybulec <trybulec@math.uwb.edu.pl>]

When adjectives had been introduced in Mizar (and attributes - the 
constructors for adjectives), a huge revision of MML
was necessary.

So, for unary predicates (actually predicates that have only one visible 
argument) and modes with all loci occurring
in the Mother Type attributes were introduced.

To simplify the revision we adopted the rule that the symbols for 
attributes originated from modes have form
       Mode-Symbol'-like'

the argument was that it looks so stupid that users will be tempted to 
introduce reasonable synonyms, and all these
'Function-like' and so on will be eliminated.

We got a new Mizar style, instead. :-)


The same goes for predicates. Quite often they had the form
       ' X is_AAA...'
then the symbol for the adjective was
           'being_AAA'
With the same argument as for '...-like' only stronger. In this way we 
got Present Continuous like
          x is being_Tarski.
To avoid it the predicate format was allowed as a synonym for the 
attributive formulas

So, instead of
           'f is being_not_0'      (meaning 0 does not belongs to the 
range of f'
it is allowed to write
           'f is_not_0'
'is_not_0' - the original Predicate Symbol.

I started to clean it. E.g. I believe 'Tarski' is quite good adjective 
and I replaced with it the symbol 'being_Tarski'.

I believe we should prohibit the predicate formats for Attributive 
Formulae. As yet I got
one supporter - Czeslaw Bylinski. Or it is the other way around, I 
support his opinion.

Regards,
Andrzej