The Mizar language is sensitive to the environment in which the article is checked. The good example is parsing of so called 'long terms'. It is also a good example for the necessity of a rather complicated algorithm used to solve rather simple task. Another such example: binding the free variables.
The linguistic superstructure is very important in our project. Many apparently logical mechanisms may be substituted by language mechanisms. The use of adjectives is an adequate example. The new implementation of it: static reconstruction of their arguments rather than the dynamic one, resulted in a cleaner semantic and better organized data base.
Recently we work more on the concept of obviousness. Particularly on using more computer algebra in the verifier.
The stress was put in this year on better structure of the Mizar Mathematical Library. It was many times revised. The beginnings what we call EMM - 'An Encyclopedia of Mathematics in Mizar' started.