[mizar] A changed in the Mizar synatx

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

Following

http://mizar.uwb.edu.pl/forum/archive/0006/msg00003.html


Hi:

When attributes were introduced in Mizar, a huge revision of the library 
changing some modes and predicates into attributes was carried out. To 
simplify the revision we adopted a temporary (hopefully) solution:
- attributes originating from modes got the '-like' postfix, and - 
attributes originating from predicates with symbols like 'is_XXX' got 
the 'being_XXX' symbol (similarly for predicates of the form 'has_XXX'
the new attribute symbol was 'having_XXX' and for 'satisfies_XXX' it was 
'satisfying_XXX'.

In this way we got something like Present Continuous in Mizar:

E is being_a_model_of_ZF

or

OAS is satisfying_DES

It looked awful and we hoped that the Authors would propose better 
notation. What we got instead is a specific "Mizar style" as new authors 
mimicked these 'rules' in their notation :-)
For attributes originating from predicates we decided to keep the 
predicate format as a synonym:

E is_a_model_of_ZF

or

OAS satisfies_DES

Recently, however, we have decided to eliminate these synonyms 
completely. The repository has became smaller, and the grammar can be 
simplified a bit now.

Regards,
Andrzej Trybulec